proposition: Lemma bin_conv_inv1 (f: nat -> int) n: bin_conv_inv f n = \sum_(i<n.+1) with_sgn i (f (n- i)%N) *+ 'C(n,i).
proof: Proof. rewrite /bin_conv_inv big_distrr /=. rewrite - (big_mkord xpredT (fun i => with_sgn i (f (n- i)%N) *+ 'C(n,i))). rewrite big_nat_rev /= big_mkord; apply: eq_bigr; move => [i] /=. rewrite ltnS => lin _. rewrite add0n subnS subSKn bin_sub // subKn // mulrnAr mulrA. congr (_ * _ *+ _). by rewrite -(signr_odd _ (n-i)) -exprD (oddB lin) - oddD signr_odd. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq choice fintype binomial) mathcomp(bigop ssralg poly ssrint) gaia(ssete7)