proposition: Lemma Vandermonde k l i : \sum_(j < i.+1) 'C(k, j) * 'C(l, i - j) = 'C(k + l , i).
proof: Proof. pose f k i := \sum_(j < i.+1) 'C(k, j) * 'C(l, i - j). suffices{k i} fxx k i: f k.+1 i.+1 = f k i.+1 + f k i. elim: k i => [i | k IHk [|i]]; last by rewrite -/(f _ _) fxx /f !IHk -binS. by rewrite big_ord_recl big1_eq addn0 mul1n subn0. by rewrite big_ord_recl big_ord0 addn0 !bin0 muln1. rewrite {}/f big_ord_recl (big_ord_recl (i.+1)) !bin0 !mul1n. rewrite -addnA -big_split /=; congr (_ + _). by apply: eq_bigr => j _; rewrite -mulnDl. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(div fintype tuple finfun bigop prime finset)