proposition: Lemma bin_invert_odd n: odd n -> odd(bin_invert n).
proof: Proof. move => on; rewrite (oddE on). case: (n./2) => // m;rewrite /bin_invert bin_of_nato /=; case: (map _ _) => //. by move => a l /=; rewrite natTrecE odd_double. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq choice fintype order bigop ssralg) mathcomp(div ssrnum ssrint rat prime path binomial) mathcomp(tuple finset) gaia(fibm)