lean_workbook_plus_41350

Proved

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

Prove that for all real numbers a,b,c \n\n $ab(a-c)(c-b)+bc(b-a)(a-c)+ca(c-b)(b-a)\leq0$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_41350 : ∀ a b c : ℝ, a * b * (a - c) * (c - b) + b * c * (b - a) * (a - c) + c * a * (c - b) * (b - a) ≤ 0   :=  by sorry

Source