Prove2Me

lean_workbook_plus_61185

Proved

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

Let a≥b≥c>0.a\geq b\geq c>0. Prove that

(a−b+c)(1a+b−1b+c+1c+a)≤12.(a-b+c)\left(\frac{1}{a+b}-\frac{1}{b+c}+\frac{1}{c+a}\right)\leq\frac{1}{2}.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_61185 (a b c : ℝ) (h1 : a ≥ b ∧ b ≥ c ∧ c > 0) :
  (a - b + c) * (1 / (a + b) - 1 / (b + c) + 1 / (c + a)) ≤ 1 / 2   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph