Prove2Me

lean_workbook_plus_58693

Proved

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

If x,yx, y are positive reals such that (x−y)(x−1)≤0(x-y)(x-1)\le 0 then prove that x+2yy+2x≥y+2xyx+2xy\dfrac{x+2y}{y+2x}\ge \dfrac{y+2xy}{x+2xy}

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_58693 (x y : ℝ) (hx : 0 < x) (hy : 0 < y) (hxy : 0 < x + y) (h : (x - y) * (x - 1) ≤ 0) : (x + 2 * y) / (y + 2 * x) ≥ (y + 2 * x * y) / (x + 2 * x * y)   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph