lean_workbook_plus_67932

Proved

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

$(a+b)^3\le 4(a^3+b^3)\iff 3(a+b)(a-b)^2\ge 0$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_67932 (a b : ℝ) : (a + b) ^ 3 ≤ 4 * (a ^ 3 + b ^ 3) ↔ 3 * (a + b) * (a - b) ^ 2 ≥ 0   :=  by sorry

Source