proposition: Lemma bin_conv_inv3 (f g: nat -> int) n: (forall i, i<=n -> f i = bin_conv_inv g i) -> (forall i, i<=n -> g i = bin_conv_dir f i).
proof: Proof. move => H. pose g' i := with_sgn i (g i); pose f' i := with_sgn i (f i). have H': forall i, i <= n -> f' i = bin_conv_dir g' i. by move => i lin; rewrite /f' (H _ lin) /g' double_pow_m1. move => i lin; move: (bin_conv_inv2 H' lin);rewrite /g' /bin_conv_inv => h. move: (f_equal (fun z => (-1) ^+ i *z) h);rewrite !double_pow_m1. by move => ->; apply : eq_bigr => j _; rewrite /f' double_pow_m1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq choice fintype binomial) mathcomp(bigop ssralg poly ssrint) gaia(ssete7)