exact (ne_of_lt this)
case inr.inr.inr
u f : ℝ → ℝ
hf : ∀ (x y : ℝ), f (x + y) = f x * u y + f y
hy0 : ∀ (x : ℝ), f x = f x * 1 + f 0
h00 : u 0 = 1
hf0 : f 0 = 0
x : ℝ
hx : x ≠ 0
hm2 : StrictAnti f
h3 : 0 < x
this : f x < 0
⊢ f x ≠ 0
no goals