proposition: Lemma bin_conv_inv2 (f g: nat -> int) n: (forall i, i<=n -> f i = bin_conv_dir g i) -> (forall i, i<=n -> g i = bin_conv_inv f i).
proof: Proof. move => h. have h1:forall i m, m <=n -> i <= m -> f i = \sum_(j<m.+1) (g j) *+ 'C(i,j). move => i m lemn leim; rewrite (h _ (leq_trans leim lemn)). rewrite - ltnS in leim; rewrite - (subnKC leim) big_split_ord /=. rewrite - (addr0 (bin_conv_dir g i)); congr (_ + _); rewrite big1 //. by move => [k kn] _ /=; rewrite bin_small // leq_addr. move => i lein; rewrite /bin_conv_inv. have ->: \sum_(i0 < i.+1) with_sgn i0 (f i0) *+ 'C(i, i0) = \sum_(k < i.+1) (\sum_(j<i.+1) (g j) * ((-1) ^+ k *+ ('C(i,k) * 'C(k, j)))). apply: eq_bigr ; move => [k lk] _ /=. transitivity (\sum_(j<i.+1) (g j) * (-1) ^+ k *+ 'C(k, j) *+ 'C(i,k)). rewrite sumrMnl; congr (_ *+ _). rewrite (h1 k i lein) // big_distrr /=; apply: eq_bigr => j _. by rewrite mulrnAr mulrC. by apply: eq_bigr => j _; rewrite - ! mulrnAr - !mulrnA mulnC. rewrite exchange_big /= big_ord_recr /= big1. rewrite add0r - big_distrr /= (bin_invb (leqnn i)) subnn mulr1. by rewrite (mulrC (g i)) double_pow_m1. move => [j ji] _ /=; rewrite - big_distrr /= (bin_invb (ltnW ji)). by rewrite - (subnSK ji) ! mulr0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq choice fintype binomial) mathcomp(bigop ssralg poly ssrint) gaia(ssete7)