Theorem: Mathlib.Meta.Positivity.Real.one_sub_div_exp_pos_of_pos (CvxLean/Tactic/Arith/PositivityExt.lean)

State before:
x : ℝ
h : 0 < x
⊢ 0 < 1 - 1 / x.exp
Tactic:
field_simp
State after:
x : ℝ
h : 0 < x
⊢ 0 < x.exp

State before:
x : ℝ
h : 0 < x
⊢ 0 < x.exp
Tactic:
positivity
State after:
no goals