lean_workbook_plus_14955
ProvedPreamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_14955 {x y z : ℝ} : 4 ≥ (x * y + y * z + z * x) * (4 - (x * y + y * z + z * x)) := by sorrySource
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_14955 {x y z : ℝ} : 4 ≥ (x * y + y * z + z * x) * (4 - (x * y + y * z + z * x)) := by sorry