proposition: Lemma base2rev_odd n: odd n -> base2rev n = nat_of_bin (num_of_list (rev (list_of_num (bin_of_nat n)))).
proof: Proof. move/oddE ->; case: {n} (n./2) => // n. by rewrite /base2rev bin_of_nato /= rev_cons -nat_of_list_rT. 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)