proposition: Lemma F26a (k n: nat): \sum_(i<k.+1) ( with_sign i 'C(n.+1, i)) = with_sign k 'C(n, k).
proof: Proof. move: k; elim; first by rewrite big_ord_recl /= big_ord0 ! bin0 addr0. move => k Hrec; rewrite big_ord_recr /= Hrec exprS - mulrnAr ! mulN1r. by rewrite (binS n k) -opprB - mulrnBr ? addnK ? mulNrn // leq_addl. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq choice fintype binomial) mathcomp(bigop ssralg poly ssrint) gaia(ssete7)