lean_workbook_plus_2465

Proved

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

To prove right inequality we have to prove: \n $(x+z)^2-4y(x+z)+4y^2 \ge 0$ \n $\Leftrightarrow$ $(x+z-2y)^2 \ge 0$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_2465 (x y z : ℝ) : (x + z) ^ 2 - 4 * y * (x + z) + 4 * y ^ 2 ≥ 0   :=  by sorry

Source