Stars and bars: the number of compositions of n into k parts

Stars and bars. The number of compositions of $n$ into $k+1$ nonnegative parts is

This is the classical stars-and-bars count, stated in the boxed form used throughout the mission: comps N (k+1) n is the finite set of functions $\mathrm{Fin}(k+1)\to\mathrm{Fin}(N+1)$ whose values sum to $n$, and the hypothesis $n\le N$ guarantees the box is inactive — every coordinate of such a tuple is at most $n$, hence at most $N$.

Proof. Splitting off the first coordinate identifies compositions of $n$ into $k+2$ parts with the disjoint union, over $i=0,\dots,n$, of the compositions of $n-i$ into $k+1$ parts; this gives the recurrence $c(k+1,n)=\sum_{i\le n}c(k,n-i)$ with $c(0,n)=[n=0]$. The binomial $\binom{n+k}{n}$ satisfies the same recurrence by the hockey-stick identity $\sum_{j\le n}\binom{j+k}{j}=\binom{n+k+1}{n}$, which is itself an immediate induction from Pascal's rule.

Formalization Note The count is taken inside a fixed box $\mathrm{Fin}(N+1)$ because $\mathbb{N}^{k}$ has no Fintype; holding $N$ fixed while $k$ and $n$ vary is what lets the induction avoid any reindexing of the tail.