Prove2Me

An asymmetric pairwise ratio inequality

Proved
WorkbookSource.base_31586

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

lean-workbooksource-checked

Let x,y,z>0x,y,z>0 ,prove that: yz+x(x+y)+yz+x(y+z)+x+zx+y(y+z)+zx+y(z+x)≥52z+52y.\frac{y}{z+x}(x+y)+\frac{y}{z+x}(y+z)+x+\frac{z}{x+y}(y+z)+\frac{z}{x+y}(z+x)\geq \frac{5}{2}z+\frac{5}{2}y.

Source: InternLM Lean-Workbook, record lean_workbook_31586 (Apache-2.0). Complete source proposition preserved; proof developed independently.

Preamble
import Mathlib
open Real Nat
Formal statement
theorem WorkbookSource.base_31586 (x y z : ℝ) (hx : 0 < x) (hy : 0 < y) (hz : 0 < z) : (y / (z + x)) * (x + y) + (y / (z + x)) * (y + z) + x + (z / (x + y)) * (y + z) + (z / (x + y)) * (z + x) ≥ (5 / 2) * z + (5 / 2) * y  :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, record lean_workbook_31586; Apache-2.0

View graph