ring
u : ℝ → ℝ
k : ℝ
hk : ∀ (x : ℝ), u x = (k * x).exp
hknz : k ≠ 0
f : ℝ → ℝ := fun x => (k * x).exp - 1
hfm : StrictMono f ∨ StrictAnti f
x y : ℝ
⊢ (k * x).exp * (k * y).exp - 1 = ((k * x).exp - 1) * (k * y).exp + ((k * y).exp - 1)
no goals