Prove2Me

lean_workbook_plus_18581

Proved

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

The given inequality is equivalent to a3−c3≥3b(a−c)(a+c−b)  ⟺  a2+ac+c2≥3b(a+c−b)a^3-c^3 \geq 3b(a-c)(a+c-b) \iff a^2+ac+c^2 \geq 3b(a+c-b) , which with the hypotheses b=c+r,a=c+r+sb=c+r, a=c+r+s ( r,s∈R+r, s \in \mathbb{R}^+ ) becomes (r−s)2≥0(r-s)^2 \geq 0 .

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_18581  (b c a r s : ℝ)
  (h₀ : 0 < r ∧ 0 < s)
  (h₁ : b = c + r)
  (h₂ : a = c + r + s) :
  (a^3 - c^3 - 3 * b * (a - c) * (a + c - b) ≥ 0) ↔ (a^2 + a * c + c^2 - 3 * b * (a + c - b) ≥ 0)   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph