lean_workbook_plus_63464

Proved

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

Equivalent to.. $c^2-(a+b)c+\frac {(a+b)^2}{4}\geq 0$ which is obvious since $(c-\frac {a+b}{2})^2\geq 0$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_63464 (a b c : ℝ) : (c^2 - (a + b) * c + (a + b)^2 / 4) ≥ 0   :=  by sorry

Source