A two-variable rational product lower bound

Proved

WorkbookSource.base_5787

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

lean-workbooksource-checked

Let $x,y>0.$ Prove that

\left(x+\frac{2}{y} \right) \left(\frac{y}{x}+2 \right)\geq 8

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

Preamble

import Mathlib
open Real Nat

Formal statement

theorem WorkbookSource.base_5787 (x y : ℝ) (hx : 0 < x) (hy : 0 < y) : (x + 2/y) * (y/x + 2) ≥ 8  :=  by sorry

Source