lean_workbook_plus_26059

Proved

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

Nesbitt's Inequality: For any three positive reals $a$ , $b$ , and $c$ , we have that

\frac{a}{b+c}+\frac{b}{c+a}+\frac{c}{a+b}\geq\frac{3}{2}.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_26059 {a b c : ℝ} (h : 0 < a ∧ 0 < b ∧ 0 < c) : (a / (b + c) + b / (c + a) + c / (a + b)) ≥ 3 / 2   :=  by sorry

Source