x✝ y✝ x y : ℝ
h : x < y
⊢ exp x < exp (y - x) * exp x
x✝ y✝ x y : ℝ
h : x < y
⊢ exp x < exp y
rw [← sub_add_cancel y x, Real.exp_add]
no goals
x✝ y✝ x y : ℝ
h : x < y
⊢ exp x < exp (y - x) * exp x
exact (lt_mul_iff_one_lt_left (exp_pos _)).2
    (lt_of_lt_of_le (by linarith) (add_one_le_exp_of_nonneg (by linarith)))
no goals
x✝ y✝ x y : ℝ
h : x < y
⊢ 1 < y - x + 1
linarith
no goals
x✝ y✝ x y : ℝ
h : x < y
⊢ 0 ≤ y - x
linarith