lean_workbook_plus_67003

Open

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

Prove that $\sqrt{1+(\pi-x)^2}-\sqrt{1+x^2} \ge 0$ $\forall x \in [0,\frac{\pi}{2}]$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_67003 (x : ℝ) (hx : 0 ≤ x ∧ x ≤ π/2) : 0 ≤ Real.sqrt (1 + (π - x) ^ 2) - Real.sqrt (1 + x ^ 2)   :=  by sorry

Source