proposition: Lemma bin_conv_inv_rec (f g: nat -> int) n: (forall i, i<=n.+1 -> g i = bin_conv_inv f i) -> (g n) + (g n.+1) = bin_conv_inv (fun i => (f i.+1)) n.
proof: Proof. move => h. rewrite addrC (h _ (ltnSn n)) (h _ (leqnSn n)) !bin_conv_inv1 {h}. rewrite big_ord_recl [X in _ = X] big_ord_recl /= - addrA !subn0 ! bin0. rewrite [X in _ + (X + _) = _] (_:_ = \sum_(i < n.+1) with_sgn i.+1 (f (n.+1 - i.+1)%N) *+ 'C(n, i.+1) - \sum_(i < n.+1) with_sgn i (f (n - i)%N) *+ 'C(n, i)). rewrite addrAC addrK; congr (_ + _). rewrite big_ord_recr /= (bin_small (ltnSn n)) mulr0n addr0. apply: eq_bigr; move=> [i lin] _ /=; rewrite subSn //. rewrite -sumrB /=; apply: eq_bigr; move=> [i lin] _ /=. rewrite -mulNrn - mulNr exprS mulN1r - mulrnDr //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq choice fintype binomial) mathcomp(bigop ssralg poly ssrint) gaia(ssete7)