have hkn' : k < 0 := by
  simp only [not_lt] at *
  exact Ne.lt_of_le hknz hkn
case inr.h
u : ℝ → ℝ
k : ℝ
hk : ∀ (x : ℝ), u x = (k * x).exp
hknz : k ≠ 0
f : ℝ → ℝ := fun x => (k * x).exp - 1
hkn : ¬0 < k
x y : ℝ
hxy : x < y
⊢ f y < f x
case inr.h
u : ℝ → ℝ
k : ℝ
hk : ∀ (x : ℝ), u x = (k * x).exp
hknz : k ≠ 0
f : ℝ → ℝ := fun x => (k * x).exp - 1
hkn : ¬0 < k
x y : ℝ
hxy : x < y
hkn' : k < 0
⊢ f y < f x