Nat.add_choose_eq

theorem Nat.add_choose_eq : ∀ (m n k : ℕ), (m + n).choose k = (Finset.antidiagonal k).sum fun ij => m.choose ij.1 * n.choose ij.2

This theorem expresses Vandermonde's identity in combinatorial terms. For any non-negative integers `m`, `n`, and `k`, the number of ways to choose `k` items from a group of `m + n` items is equal to the sum, for all integer pairs `(i, j)` in the set of antidiagonals of `k`, of the product of the number of ways to choose `i` items from `m` and `j` items from `n`. This sums over all possible ways of splitting `k` into two parts `i` and `j` such that `i + j = k`.

More concisely: The number of ways to choose `k` items from a set of `m + n` items is equal to the sum, over all `0 ≤ i ≤ k` and `0 ≤ j ≤ k` with `i + j = k`, of the product of the number of combinations of `m` items taken `i` at a time and the number of combinations of `n` items taken `j` at a time.