Lean-Workbook Syntax 69256: The hockey-stick binomial identity

For natural numbers $n,m$, $\sum_{k=0}^{m}\binom{n+k}{k}=\binom{n+m+1}{m}$.

Source: Lean-Workbook row lean_workbook_plus_69256 (Apache-2.0), original record. This corrected declaration replaces the obsolete finite sum/product binder in with ∈ and restores required imports or namespaces. Ranges, casts, quantifiers, and mathematical expressions are preserved.