lean_workbook_plus_62199

Proved

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

A square of a real number is always greater than or equal to zero, i.e. $(x-y)^2\geq 0$ for real $x$ and $y$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_62199 (x y : ℝ) : (x - y) ^ 2 ≥ 0   :=  by sorry

Source