proposition: Lemma G6_a (n p:nat) (a b: int): (\sum_(i < p.+1) a^+ (p-i) * b ^+ i *+ ('C(n, i) * 'C(n-i, p-i)) = (a+b) ^+ p *+ 'C(n , p) )%Z.
proof: Proof. have: (n < p) || (p <= n) by rewrite ltnNge orNb. case /orP => lenp. rewrite bin_small // mulr0n big1 //; move => [i lip] _ /=. move: lip; rewrite ltnS leq_eqVlt; case /orP => lipp. by move /eqP:lipp => ->; rewrite bin_small. move: (ltn_sub2r lipp lenp) => h;rewrite (bin_small h) muln0 //. have leq1: n - p < n.+1 by rewrite ltnS leq_subr. move: (power_monom (a+b) n) => eq1. move: (f_equal (coefp (n - p)%N) eq1) => /=; rewrite coef_poly leq1/=. rewrite (subKn lenp) (bin_sub lenp) => <-. rewrite polyCD addrA exprDn coef_sum /=. move: (lenp); rewrite - ltnS => lenp'. have aux: forall i : nat, p < i < n.+1 -> (('X + a%:P) ^+ (n - i) * b%:P ^+ i *+ 'C(n, i))`_(n - p) = 0. move => i /andP [i1 i2]; rewrite coefMn - polyC_exp coefMC power_monom. rewrite ltnS in i2; move: (ltn_sub2l (leq_trans i1 i2) i1). rewrite coef_poly ltnS ltnNge ;case ((n - p <= n - i)) => // _. by rewrite mul0r mul0rn. rewrite (shorten_sum lenp' aux); apply eq_bigr; move => [i lin] _ /=. rewrite coefMn - polyC_exp coefMC mulnC mulrnA power_monom; congr (_ *+ _). rewrite ltnS in lin; move: (leq_sub2l n lin) => le3. rewrite coef_poly ltnS le3 - (bin_sub le3). have ->: ((n - i - (n - p)) = p - i) %N. by rewrite - {1} (subnK lenp) -{2} (subnK lin) addnA addnK addnC addnK. by rewrite mulrC - mulrnAr mulrC. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq choice fintype binomial) mathcomp(bigop ssralg poly ssrint) gaia(ssete7)