lean_workbook_plus_47238

Proved

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

Claim 2. Let $x,y$ be nonnegative reals. Then\n\n

\frac{1}{2x+1}+\frac{1}{2y+1}\ge\frac{2}{xy+2}.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_47238 (x y : ℝ) (hx : 0 ≤ x) (hy : 0 ≤ y) : (1 / (2 * x + 1) + 1 / (2 * y + 1)) ≥ 2 / (x * y + 2)   :=  by sorry

Source