lean_workbook_plus_2994
ProvedShow that for all real numbers x and y.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_2994 (x y : ℝ) : (x - y) ^ 2 + (x - 1) ^ 2 + (y - 1) ^ 2 ≥ 0 := by sorry
Source
Show that for all real numbers x and y.
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_2994 (x y : ℝ) : (x - y) ^ 2 + (x - 1) ^ 2 + (y - 1) ^ 2 ≥ 0 := by sorry