lean_workbook_plus_38119
ProvedProve that
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_38119 (a b : ℝ) : a^2 * b^2 + (a^2 + b^2) * (a + b)^2 + 3 - 6 * a * b * (a + b) ≥ 0 := by sorry
Source
Prove that
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_38119 (a b : ℝ) : a^2 * b^2 + (a^2 + b^2) * (a + b)^2 + 3 - 6 * a * b * (a + b) ≥ 0 := by sorry