lean_workbook_plus_4319

Proved

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

Inequality is equivalent to: $P(a)=2a^2-2a(b+c-3)+2(b^2+c^2)-2bc+6(1-b)\ge 0$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_4319 (a b c : ℝ) : 2*a^2 - 2*a*(b + c - 3) + 2*(b^2 + c^2) - 2*b*c + 6*(1 - b) ≥ 0   :=  by sorry

Source