lean_workbook_plus_20262

Proved

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

Other idea: for $n>1$ we have: $(n+1)^2<n^2+3n<(n+2)^2$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_20262 (n : ℕ) (hn : 1 < n) : (n + 1) ^ 2 < n ^ 2 + 3 * n ∧ n ^ 2 + 3 * n < (n + 2) ^ 2   :=  by sorry

Source