proposition: Lemma bin_invb (j q: nat): j <= q -> \sum_(k<q.+1) with_sign k ('C(q, k) * 'C(k, j)) = with_sgn j (Posz(q - j == 0)%N).
proof: Proof. move => h. rewrite - [in X in (X = _)] (subnKC h) - addnS big_split_ord /=. rewrite big1 ? add0r; last by move => [i lin] _; rewrite (bin_small lin) muln0. rewrite - (bin_inva j (q-j)) big_distrr /=; apply: eq_bigr. by move => [i len] _ /=; rewrite mulrnAr exprD. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq choice fintype binomial) mathcomp(bigop ssralg poly ssrint) gaia(ssete7)