lean_workbook_plus_59057

Proved

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

Let $x,y,z > 0$ , prove that \n $\frac {x}{y} + \frac {y}{z} + \frac {z}{x}\geq\frac {x + y}{y + z} + \frac {y + z}{x + y} + 1.$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_59057 (x y z : ℝ) (hx : 0 < x) (hy : 0 < y) (hz : 0 < z) : (x / y + y / z + z / x) ≥ (x + y) / (y + z) + (y + z) / (x + y) + 1   :=  by sorry

Source

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

View graph