proposition: Lemma bin_vandermonde (k l i:nat): (\sum_(j < i.+1) ('C(k, j) *'C(l, (i - j))))%N = 'C(k+l , i)%N.
proof: Proof. apply: intmul_inj; set z1 := ('X + 1%:P) :{poly int}. have aux: forall t j, (z1 ^+ t)`_j = 'C (t, j) %Z. move=> t j; rewrite /z1 (power_monom _ t) coef_poly expr1n. by case (ltnP j t.+1) => h //; rewrite ?pmulrn ?intz // bin_small. move:(f_equal (fun z:{poly int} => z`_ i) (exprD z1 k l)). rewrite coefM aux;move => ->;rewrite sumMz intz. by apply: eq_bigr => j _;rewrite !aux intz PoszM. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq choice fintype binomial) mathcomp(bigop ssralg poly ssrint) gaia(ssete7)