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

State before:
x : ℝ
h : 0 < x - 1
⊢ 1 < x
Tactic:
linarith
State after:
no goals