induction' n with pn hpn
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
h1 : ∀ (n : ℕ) (x : ℝ), u (↑n * x) = u x ^ n
h2 : ∀ (x : ℝ), u x * u (-x) = 1
hunz : ∀ (x : ℝ), 0 < u x
h3 : ∀ (x : ℝ), u (-x) = 1 / u x
h4 : ∀ (z : ℤ) (x : ℝ), u (↑z * x) = u x ^ z
k : ℝ
hk : k.exp = u 1
hnexp : ∀ (n : ℕ), u ↑n = (k * ↑n).exp
hzexp : ∀ (z : ℤ), u ↑z = (k * ↑z).exp
x : ℝ
p : ℕ
hp : 0 < p + 1
n : ℕ
⊢ u (x / ↑p.succ) ^ n = u (x * ↑n / ↑p.succ)
case zero
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
h1 : ∀ (n : ℕ) (x : ℝ), u (↑n * x) = u x ^ n
h2 : ∀ (x : ℝ), u x * u (-x) = 1
hunz : ∀ (x : ℝ), 0 < u x
h3 : ∀ (x : ℝ), u (-x) = 1 / u x
h4 : ∀ (z : ℤ) (x : ℝ), u (↑z * x) = u x ^ z
k : ℝ
hk : k.exp = u 1
hnexp : ∀ (n : ℕ), u ↑n = (k * ↑n).exp
hzexp : ∀ (z : ℤ), u ↑z = (k * ↑z).exp
x : ℝ
p : ℕ
hp : 0 < p + 1
⊢ u (x / ↑p.succ) ^ 0 = u (x * ↑0 / ↑p.succ)

case succ
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
h1 : ∀ (n : ℕ) (x : ℝ), u (↑n * x) = u x ^ n
h2 : ∀ (x : ℝ), u x * u (-x) = 1
hunz : ∀ (x : ℝ), 0 < u x
h3 : ∀ (x : ℝ), u (-x) = 1 / u x
h4 : ∀ (z : ℤ) (x : ℝ), u (↑z * x) = u x ^ z
k : ℝ
hk : k.exp = u 1
hnexp : ∀ (n : ℕ), u ↑n = (k * ↑n).exp
hzexp : ∀ (z : ℤ), u ↑z = (k * ↑z).exp
x : ℝ
p : ℕ
hp : 0 < p + 1
pn : ℕ
hpn : u (x / ↑p.succ) ^ pn = u (x * ↑pn / ↑p.succ)
⊢ u (x / ↑p.succ) ^ (pn + 1) = u (x * ↑(pn + 1) / ↑p.succ)