Prove2Me

lean_workbook_plus_61846

Proved

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

Prove the inequality: (a−b)(c−a)(b−c)<abc(a-b)(c-a)(b-c) < abc for a, b, and c being the lengths of the edges of a triangle.

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_61846 (a b c : ℝ) (hx: a > 0 ∧ b > 0 ∧ c > 0) (hab : a + b > c) (hbc : b + c > a) (hca : a + c > b) : (a - b) * (c - a) * (b - c) < a * b * c   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph