Equivalent cyclic fraction identities

Proved

WorkbookSource.problem_28330

by wamlart · Sep 12, 2026 · Mathlib 0df444a (Lean v4.33.1)

lean-workbooksource-checked

Let $x,y,z>0$ and $x^2+y^2+z^2+2xyz=1.$ Prove that

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

\iff

\frac{x}{x+yz}+\frac{y}{y+zx}+\frac{z}{z+xy}=2

Source: InternLM Lean-Workbook, record lean_workbook_28330 (Apache-2.0). The complete source proposition and its explicit variable declarations are preserved.

Preamble

import Mathlib
open Real

Formal statement

theorem WorkbookSource.problem_28330 (x y z : ℝ) (hx : 0 < x) (hy : 0 < y) (hz : 0 < z) (h : x^2 + y^2 + z^2 + 2 * x * y * z = 1) : (x * y / (x * y + z) + y * z / (y * z + x) + z * x / (z * x + y) = 1 ↔ x / (x + y * z) + y / (y + z * x) + z / (z + x * y) = 2)  :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, record lean_workbook_28330; Apache-2.0

View graph