lean_workbook_plus_4026

Proved

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

For $x,y,z,t \in R$ prove that $2(x-y)(y-z)(z-t)(t-x)+(x-z)^2(y-t)^2 \ge 0$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

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

Source