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 : Nat) : Eq ((HAdd.hAdd m n).choose k) ((Finset.HasAntidiagonal.antidiagonal k).sum fun (ij : Prod Nat Nat) => HMul.hMul (m.choose ij.fst) (n.choose ij.snd))

Vandermonde's identity