lean_workbook_plus_43770

Proved

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

Prove that for $x, y, z \in \mathbb{R}$ , $y^4z^2 + z^4x^2 + x^4y^2 \geq yzx(zx^2 + y^2x + z^2y)$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_43770 (x y z : ℝ) : y^4 * z^2 + z^4 * x^2 + x^4 * y^2 ≥ y * z * x * (z * x^2 + y^2 * x + z^2 * y)   :=  by sorry

Source