proposition: Lemma G6_b (n p:nat): p <> 0%N -> \sum_(i < p.+1) (-1%:Z) ^+ i *+ ('C(n, i) * 'C(n-i, p-i)) = 0.
proof: Proof. move => pnz; move: (G6_a n p 1%:Z (-1%:Z)). rewrite addrN (_ : 0 ^+ p = 0) ? mul0rn; last first. by move: pnz; case:p => // p;rewrite exprS mul0r. by move => eq; rewrite - {2} eq; apply: eq_bigr => i _; rewrite expr1n mul1r. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq choice fintype binomial) mathcomp(bigop ssralg poly ssrint) gaia(ssete7)