Prove2Me

lean_workbook_plus_28782

Proved

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

another inequality with the same condition Prove (a+b−c)(b+c−a)(c+a−b)abc≥0(a+b-c)(b+c-a)(c+a-b)abc\geq 0

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

View graph