lean_workbook_plus_4427

Proved

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

Let $a, b, c, d$ be real numbers with $a+d=b+c$ Prove that $(a-b)(c-d)+(a-c)(b-d)+(d-a)(b-c)\geq0$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_4427 (a b c d : ℝ) (h : a + d = b + c) :
  (a - b) * (c - d) + (a - c) * (b - d) + (d - a) * (b - c) ≥ 0   :=  by sorry

Source