lean_workbook_plus_8838

Proved

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

$(a+c)^2(b+c)^2 \ge 4c(a+b)(c^2+ab)$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_8838 (a b c : ℝ) : (a + c) ^ 2 * (b + c) ^ 2 ≥ 4 * c * (a + b) * (c ^ 2 + a * b)   :=  by sorry

Source