lean_workbook_plus_12651

Proved

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

$(a^2+1)(b^2+1)(c^2+1) \ge (a+b+c-abc)^2=(7-abc)^2$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_12651 (a b c : ℝ) : (a^2+1)*(b^2+1)*(c^2+1) ≥ (a+b+c-a*b*c)^2   :=  by sorry

Source