lean_workbook_plus_79241

Proved

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

Prove that if, $x,y>0$ \n\n $x^3+y^3 \ge xy(x+y)\ \ \ \left( \iff (x-y)^2(x+y) \ge 0 \right)$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_79241 (x y : ℝ) (hx : 0 < x) (hy : 0 < y) : x^3 + y^3 ≥ x * y * (x + y)   :=  by sorry

Source