cases' hm with hm hm <;> nlinarith [hm hx0, hm hgt]
case inr.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
x : ℝ
H : u x ≤ 0
hgt : 0 < x
h10 : u x * u (-x) = 1
hx0 : -x < 0
⊢ False
no goals