lean_workbook_plus_72488

Proved

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

Simplify $2+\frac{|a|+|b|}{2008} \geq 1 + \frac {|a-b|}{2008}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_72488 : ∀ a b : ℝ, 2 + (|a| + |b|) / 2008 ≥ 1 + |a - b| / 2008   :=  by sorry

Source