lean_workbook_plus_29927

Proved

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

Let $x, y, z$ be nonnegative positive integers. Prove that \n

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

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_29927 (x y z : ℕ) : (x / (z * x + 2 * x + 1) + y / (x * y + 2 * y + 1) + z / (y * z + 2 * z + 1) ≤ 3 / 4 ∧ 3 / 4 ≤ x / (x * y + 2 * y + 1) + y / (y * z + 2 * z + 1) + z / (z * x + 2 * x + 1))   :=  by sorry

Source

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

View graph