feat(data/real/cau_seq): Make power elementwise (#17124)
Redefine `nsmul`, `zsmul`, `pow` elementwise on Cauchy sequences. This gives a few lemmas for free (as they're now refl).
Add some forgotten `coe` and `const` lemmas and tag some more with `norm_cast`.
