lean_workbook_plus_51149

Proved

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

Let $k^2\leq n < (k+1)^2$ , so $n=k^2+r$ for some $0\leq r < 2k+1$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_51149 (n : ℕ) (k : ℕ) (h₁ : k^2 ≤ n) (h₂ : n < (k + 1)^2) : ∃ r : ℕ, n = k^2 + r ∧ r < 2 * k + 1   :=  by sorry

Source