Prove2Me

lean_workbook_plus_80056

Proved

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

prove that 1−a1+a+ab−b1+b+bc−c1+c+ca=(abc−1)2(1+a+ab)(1+b+bc)(1+c+ca)≥01-\frac{a}{1+a+ab}-\frac{b}{1+b+bc}-\frac{c}{1+c+ca}=\frac{(abc-1)^2}{(1+a+ab)(1+b+bc)(1+c+ca)}\geq0 given a,b,c>0a,b,c>0

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_80056 (a b c : ℝ) (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) : (1 - a / (1 + a + a * b) - b / (1 + b + b * c) - c / (1 + c + c * a) : ℝ) = (a * b * c - 1) ^ 2 / ((1 + a + a * b) * (1 + b + b * c) * (1 + c + c * a))   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph