have : ↑pn * x + x = (↑pn + 1) * x := by ring
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
pn : ℕ
hpn : ∀ (x : ℝ), u (↑pn * x) = u x ^ pn
x : ℝ
⊢ ↑pn.succ * x = ↑pn * x + x
u : ℝ → ℝ
hu : ∀ (x y : ℝ), u (x + y) = u x * u y
hu0 : u 0 = 1
hm : StrictMono u ∨ StrictAnti u
pn : ℕ
hpn : ∀ (x : ℝ), u (↑pn * x) = u x ^ pn
x : ℝ
this : ↑pn * x + x = (↑pn + 1) * x
⊢ ↑pn.succ * x = ↑pn * x + x