lean_workbook_plus_31349

Proved

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

Prove that $(\frac {p - 1}{2})^2 + \frac {p - 1}{2} + 1 = \frac {p^2 + 3}{4}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_31349  (p : ℕ)
  (h₀ : p > 0)
  (h₁ : p % 2 = 1) :
  ((p - 1) / 2)^2 + (p - 1) / 2 + 1 = (p^2 + 3) / 4   :=  by sorry

Source