lean_workbook_plus_58926

Proved

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

Let $2>a\geq 0$ . Prove that \n

\frac{a}{2-a}+ \frac{2}{a+1}\geq \frac{5}{3}

Equality holds when $a=\frac{1}{2}.$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_58926 (a : ℝ) (ha : 2 > a ∧ a >= 0) : a / (2 - a) + 2 / (a + 1) ≥ 5 / 3 ∧ (a = 1 / 2 → a / (2 - a) + 2 / (a + 1) = 5 / 3)   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph