proposition: Lemma G6_c (n p:nat): (\sum_(i < p.+1) 'C(n, i) * 'C(n-i, p-i) = 2 ^ p *'C(n , p) )%N.
proof: Proof. apply: intmul_inj. move: (G6_a n p 1 1); rewrite - mulr2n - natrX - mulrnA sumMz. rewrite (_: (2 ^ p * 'C(n, p))%:R = (2 ^ p * 'C(n, p))%N%:~R) //. by move => <-; apply: eq_bigr => i _; rewrite 2! expr1n mul1r //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq choice fintype binomial) mathcomp(bigop ssralg poly ssrint) gaia(ssete7)