proposition: Lemma F36 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)). rewrite -/(f k i) ; move: k i. have fx0: forall k, f k 0 = 'C(k + l, 0). by move=> k; rewrite /f big_ord_recl big_ord0 addn0 !bin0 muln1. have f0x: forall i, f 0 i = 'C(l, i). move=> i; rewrite /f big_ord_recl bin0 mul1n big1 ? addn0 ?subn0 //. suff fxx: forall k i, f (k.+1) (i.+1) = f k i.+1 + f k i. by elim => [//| k h1]; elim => [//| i h2]; rewrite fxx h1 h1 - binS addSn. move=> k i; rewrite /f big_ord_recl (big_ord_recl (i.+1)) !bin0 !mul1n -addnA. congr (_ + _); rewrite -big_split /=. by apply: eq_bigr => j _ ; rewrite - mulnDl. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)