lean_workbook_plus_81538

Proved

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

$\sqrt{\frac{a^{2}}{4}}\geq \sqrt{a-1}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_81538 (a : ℝ) (ha : 0 ≤ a) : Real.sqrt (a^2 / 4) ≥ Real.sqrt (a - 1)   :=  by sorry

Source