lean_workbook_plus_13937

Proved

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

Prove that $3\,{\frac { \left( y-z \right) ^{2} \left( x-z \right) ^{2} \left( x-y \right) ^{2}}{{y}^{2}{x}^{2}{z}^{2}}}\geq0$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_13937 (x y z : ℝ) : 3 * (y - z) ^ 2 * (x - z) ^ 2 * (x - y) ^ 2 / (y ^ 2 * x ^ 2 * z ^ 2) ≥ 0   :=  by sorry

Source