lean_workbook_plus_1355

Proved

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

Let x,y,z be positive real numbers, prove that:\n

\frac{y}{xy+y+1}+ \frac{z}{yz+z+1}+ \frac{x}{zx+x+1}\leq 1

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_1355 (x y z : ℝ) (hx : 0 < x) (hy : 0 < y) (hz : 0 < z) : (y / (x * y + y + 1) + z / (y * z + z + 1) + x / (z * x + x + 1)) ≤ 1   :=  by sorry

Source

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

View graph