Prove2Me

lean_workbook_plus_82383

Proved

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

proofwiki

If a a , b b and x x are positive numbers we have that 1≥ab⇔x+ax+b≥ab 1\ge\dfrac{a}{b}\Leftrightarrow\dfrac{x+a}{x+b}\ge\dfrac{a}{b} with equality if and only if a=b a=b .

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_82383 (a b x : ℝ) (ha : 0 < a) (hb : 0 < b) (hx : 0 < x) : 1 ≥ a / b ↔ (x + a) / (x + b) ≥ a / b   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph