lean_workbook_plus_52924

Proved

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

If $a-b=1$ ,\n $a^2-b^2=(a-b)(a+b)=a+b$ \n $\therefore n^2-(n-1)^2=2n-1$ $\rightarrow$ Difference between two consecutive squares

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_52924  (n : ℕ) :
  n^2 - (n - 1)^2 = 2 * n - 1   :=  by sorry

Source