chore(*): remove some defeq abuse of `^` (#18136)
There are various places where the proofs relied on the defeq of `^`, namely that
* `rfl : x ^ 0 = 1`
* `rfl : x ^ (n : ℕ) = x ^ (↑n : ℤ)`
* `rfl : x ^ (n.succ : ℕ) = x * x ^ n`
While exploiting defeq is not always a bad thing, in some of these cases it was clear that this wasn't intentional, and the author had not noticed that they were working with integer instead of natural powers.
This change is motivated by two possible refactors:
* Changing the definition of `monoid.npow_rec` to match `function.iterate`
* Changing the definition of `real.has_pow` to be the elementwise power on the cauchy sequence (#8146)
