Prove2Me

lean_workbook_plus_14163

Proved

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

If a≥c≥ba \geq c \geq b , then (a−b)(b−c)(c−a)≥0(a - b)(b - c)(c - a) \geq 0 i.e. 2(ab2+bc2+ca2)≥2(a2b+b2c+c2a),2(ab^2 + bc^2 + ca^2) \geq 2(a^2b + b^2c + c^2a), hence it rests to prove that a3+b3+c3≥a2b+b2c+c2aa^3+b^3+c^3 \geq a^2b + b^2c + c^2a which is straightforward AM-GM ∑cyca3=∑cyc(2a3+b33)≥∑cyca2b.\sum_{cyc} a^3 = \sum_{cyc}\left(\frac{2a^3 + b^3}{3}\right) \geq \sum_{cyc} a^2b.

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_14163  (a b c : ℝ)
  (h₀ : a ≥ c ∧ c ≥ b) :
  (a - b) * (b - c) * (c - a) ≥ 0   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph