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

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