Prove2Me

lean_workbook_plus_79556

Proved

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

Prove that for a,b,c≥0a, b, c \geq 0 with a≥b≥ca \geq b \geq c, the following inequalities hold:\n\n1. (a−b)3+(b−c)3+(c−a)3≤0(a-b)^3 + (b-c)^3 + (c-a)^3 \leq 0\n2. (a−b)5+(b−c)5+(c−a)5≤0(a-b)^5 + (b-c)^5 + (c-a)^5 \leq 0\n\n... and in general, (a−b)2k+1+(b−c)2k+1+(c−a)2k+1≤0(a-b)^{2k+1} + (b-c)^{2k+1} + (c-a)^{2k+1} \leq 0 for all k∈Nk \in \mathbb{N}.

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_79556 (a b c : ℝ) (h₁ : a ≥ b ∧ b ≥ c ∧ c ≥ a) (k : ℕ) :
  (a - b)^(2 * k + 1) + (b - c)^(2 * k + 1) + (c - a)^(2 * k + 1) ≤ 0   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph