proposition: Lemma bin_inva (j q: nat): \sum_(k<q.+1) with_sign k ('C(j+q, j+k) * 'C(j+k, j)) = (q==0%N).
proof: Proof. case q; first by rewrite big_ord_recl /= big_ord0 !addn0 binn muln1 expr0 addr0. move => n. set A := \sum_(k < _) _. have ->: A = \sum_(k < n.+2) (-1) ^+ k *+ 'C(n.+1, k) *+ 'C(j + n.+1, j). by apply: eq_bigr => //; move => i _ /=; rewrite - mulrnA binom_exchange1. by rewrite sumrMnl F26a bin_small // mulr0n mul0rn. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq choice fintype binomial) mathcomp(bigop ssralg poly ssrint) gaia(ssete7)