lean_workbook_plus_41409

Proved

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

For $x,y \geq 1$ , prove that $\left( x- \frac{1}{x} \right) + \left( y - \frac{1}{y} \right) \leq \left( xy- \frac{1}{xy} \right)$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_41409 (x y : ℝ) (hx : 1 ≤ x) (hy : 1 ≤ y) : (x - 1/x) + (y - 1/y) ≤ (x*y - 1/(x*y))   :=  by sorry

Source