x : ℝ
h : x < 0
h1 : 0 < -x
⊢ x + 1 < exp x
x : ℝ
h : x < 0
⊢ x + 1 < exp x
have h1 : 0 < -x := by linarith
no goals
x : ℝ
h : x < 0
h1 : 0 < -x
⊢ x + 1 < exp x
simpa [add_comm] using one_sub_lt_exp_minus_of_pos h1
no goals
x : ℝ
h : x < 0
⊢ 0 < -x
linarith