lean_workbook_plus_17115

Proved

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

Prove that for all non-negative numbers a and b, $\frac{1}{(1+a)^2}+\frac{1}{(1+b)^2}\ge \frac{2}{a^2+b^2+2}$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_17115 : ∀ a b : ℝ, a ≥ 0 ∧ b ≥ 0 → (1 / (1 + a) ^ 2 + 1 / (1 + b) ^ 2) ≥ 2 / (a ^ 2 + b ^ 2 + 2)   :=  by sorry

Source