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

State before:
x : ℝ
h : 0 < x
⊢ 0 < x.exp - 1
Tactic:
simp [h]
State after:
no goals