Prove2Me

Pascal’s binomial identity

Proved
WorkbookRestored.plus_4862

by wamlart · Sep 12, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

lean-workbookrestored-importssource-checked

For natural numbers n,mn,m,

(nm)+(nm+1)=(n+1m+1).\binom nm+\binom n{m+1}=\binom{n+1}{m+1}.

This restores the missing imports or namespaces of the original node, retaining its formal proposition. Source: Lean-Workbook row lean_workbook_plus_4862 (Apache-2.0).

Preamble
import Mathlib.Data.Nat.Choose.Basic
open Nat
Formal statement
theorem WorkbookRestored.plus_4862 (n m : ℕ) : choose n m + choose n (m + 1) = choose (n + 1) (m + 1)   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, row lean_workbook_plus_4862; original Prove2Me node ad0d3745-34e0-4cbf-8289-100aa6744fa1; Apache-2.0

View graph