lean_workbook_plus_2528

Proved

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

For all real numbers satisfying $0\leq x \leq 2$ we have $\frac{3}{1+x} \leq 3- \frac{1}{2}x^2$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_2528 (x : ℝ) (hx : 0 ≤ x ∧ x ≤ 2) : (3 / (1 + x) ≤ 3 - 1 / 2 * x ^ 2)   :=  by sorry

Source