lean_workbook_plus_32709
DisprovedTo prove becomes:
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_32709 : ∀ x y z : ℝ, (x^2 + y^2 + z^2) ≥ (x + y - z) * (x - y + z) * (y + z - x) := by sorry
Source
To prove becomes:
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_32709 : ∀ x y z : ℝ, (x^2 + y^2 + z^2) ≥ (x + y - z) * (x - y + z) * (y + z - x) := by sorry