lean_workbook_plus_19940

Proved

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

We have $\left(1-\frac{1}{1+|a|}\right)\left(1-\frac{1}{1+|b|}\right)=\frac{|a| |b|}{(1+|a|)(1+|b|)}\geq 0$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_19940 : ∀ a b : ℝ, (1 - 1 / (1 + |a|)) * (1 - 1 / (1 + |b|)) ≥ 0   :=  by sorry

Source