x✝ y x : ℝ
h : x ≤ 0
⊢ 0 < (exp (-x))⁻¹
x✝ y x : ℝ
h : x ≤ 0
⊢ 0 < exp x
rw [← neg_neg x, Real.exp_neg]
no goals
x✝ y x : ℝ
h : x ≤ 0
⊢ 0 < (exp (-x))⁻¹
exact inv_pos.2 (lt_of_lt_of_le zero_lt_one (one_le_exp (neg_nonneg.2 h)))