lean_workbook_plus_6811

Proved

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

Prove that $x^2 y^2 - x^2 y z + x^2 z^2 - x y^2 z - x y z^2 + y^2 z^2 \ge 0$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_6811 (x y z : ℝ) :
  x^2 * y^2 - x^2 * y * z + x^2 * z^2 - x * y^2 * z - x * y * z^2 + y^2 * z^2 ≥ 0   :=  by sorry

Source