lean_workbook_plus_86

Proved

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

Let $a,b,c>0$ and $\frac{1-ab}{1+b}+\frac{1-bc}{1+c}+\frac{1-ca}{1+a}=0$ . Prove that

abc\leq 1

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_86 (a b c : ℝ) (h : a > 0 ∧ b > 0 ∧ c > 0) (habc : a * b * c = 1) (h : (1 - a * b) / (1 + b) + (1 - b * c) / (1 + c) + (1 - c * a) / (1 + a) = 0) : a * b * c ≤ 1   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph