lean_workbook_plus_7582
ProvedProve that .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_7582 (x y : ℝ) : (x - y) ^ 2 * (4 * x ^ 2 + 7 * x * y + 4 * y ^ 2) ≥ 0 := by sorry
Source
Prove that .
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_7582 (x y : ℝ) : (x - y) ^ 2 * (4 * x ^ 2 + 7 * x * y + 4 * y ^ 2) ≥ 0 := by sorry