lean_workbook_plus_14572

Proved

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

Prove the inequality for $x, y, z > 0$ :\n ${\frac {x-y}{z+x}}+{\frac {y-z}{x+y}}+{\frac {z-x}{y+z}}\leq 0$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_14572 : ∀ x y z : ℝ, x > 0 ∧ y > 0 ∧ z > 0 → (x - y) / (z + x) + (y - z) / (x + y) + (z - x) / (y + z) ≤ 0   :=  by sorry

Source