proposition: Lemma F26b (n: nat): \sum_(i<n.+2) ( with_sign i 'C(n.+1, i)) = 0.
proof: Proof. by rewrite - (exprD1n (-1%:Z) (n.+1)) subrr exprS mul0r. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq choice fintype binomial) mathcomp(bigop ssralg poly ssrint) gaia(ssete7)