A squared-norm lower bound under two separation constraints

Proved

WorkbookSource.base_18542

by wamlart · Sep 13, 2026 · Mathlib 0df444a (Lean v4.33.1)

lean-workbooksource-checked

Let $a,b,c$ be real numbers, such that $a\ge b+1, b\ge c+4,$ . Prove that $a^2 + b^2 + c^2 \ge 14.$

Source: InternLM Lean-Workbook, record lean_workbook_18542 (Apache-2.0). Complete source proposition preserved; proof developed independently.

Preamble

import Mathlib
open Real Nat

Formal statement

theorem WorkbookSource.base_18542 (a b c : ℝ) (h₁ : a ≥ b + 1) (h₂ : b ≥ c + 4) : a^2 + b^2 + c^2 ≥ 14  :=  by sorry

Source