Vandermonde's identity

In this file we prove Vandermonde's identity (Nat.add_choose_eq): (m + n).choose k = ∑ (i, j) ∈ antidiagonal k, m.choose i * n.choose j

We follow the algebraic proof from https://en.wikipedia.org/wiki/Vandermonde%27s_identity#Algebraic_proof .

theorem Nat.add_choose_eq (m n k : ℕ) : (m + n).choose k = ∑ ij ∈ Finset.antidiagonal k, m.choose ij.1 * n.choose ij.2

Vandermonde's identity

theorem Nat.sum_range_choose_sq (n : ℕ) : ∑ i ∈ Finset.range (n + 1), n.choose i ^ 2 = (2 * n).choose n

The sum of entries squared in a row of Pascal's triangle