lean_workbook_plus_13414

Proved

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

If $x,y$ be positive real numbers such that $xy \geq 1$ then $\frac1{x^2+1}+\frac1{y^2+1} \geq \frac2{1+xy}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_13414 (x y : ℝ) (h : x*y ≥ 1) : (x^2 + 1)^(-1:ℤ) + (y^2 + 1)^(-1:ℤ) ≥ 2/(1 + x*y)   :=  by sorry

Source