have h11: ↑(-((↑n):ℤ)) * x = - (n * x) := by norm_num
case intro.inr
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
z : ℤ
x : ℝ
n : ℕ
hn : -↑n = z
h10 : u (↑n * x) = u x ^ n
⊢ u (↑(-↑n) * x) = u x ^ (-↑n)
case intro.inr
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
z : ℤ
x : ℝ
n : ℕ
hn : -↑n = z
h10 : u (↑n * x) = u x ^ n
h11 : ↑(-↑n) * x = -(↑n * x)
⊢ u (↑(-↑n) * x) = u x ^ (-↑n)