lean_workbook_plus_36390

Proved

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

Prove that $abc(a+b+c) \geq a^3(b+c-a) + b^3(c+a-b) + c^3(a+b-c)$ using Schur’s Inequality.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_36390 : ∀ a b c : ℝ, a * b * c * (a + b + c) ≥ a^3 * (b + c - a) + b^3 * (c + a - b) + c^3 * (a + b - c)   :=  by sorry

Source