lean_workbook_plus_9107
Proved
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_9107 : ∀ x y : ℝ, (x + y) ^ 4 - 8 * x * y * (x + y) ^ 2 + 16 * x ^ 2 * y ^ 2 ≥ 0 := by sorry
Source
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_9107 : ∀ x y : ℝ, (x + y) ^ 4 - 8 * x * y * (x + y) ^ 2 + 16 * x ^ 2 * y ^ 2 ≥ 0 := by sorry