Prove2Me

lean_workbook_plus_75400

Proved

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

Prove that (n+12)+n+1=(n+22)\binom{n+1}{2}+n+1=\binom{n+2}{2}

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_75400 (n : ℕ) : (n + 1).choose 2 + n + 1 = (n + 2).choose 2   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph