Prove2Me

lean_workbook_plus_30715

Proved

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

the following ineq is true x≥y≥z≥0x\geq y\geq z\geq0 \nx(a−b)(a−c)+y(b−a)(b−c)+z(c−b)(c−a)≥0x(a-b)(a-c)+y(b-a)(b-c)+z(c-b)(c-a) \geq0 \nso \n∑(a−c)(a−b)(b+c)2+∑ab+c≥1,5\sum \frac{(a-c)(a-b)}{(b+c)^2}+\sum \frac{a}{b+c} \geq 1,5 \nwitch is Nesbitt's ineq

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_30715 (x y z a b c : ℝ) (hx: x ≥ y ∧ y ≥ z ∧ z ≥ 0) (hab : a ≥ b ∧ b ≥ c ∧ c ≥ 0) : x * (a - b) * (a - c) + y * (b - a) * (b - c) + z * (c - b) * (c - a) ≥ 0   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph