proposition: Lemma base2rev_even n: base2rev (n.*2) = base2rev n.
proof: Proof. by case:n => // n; rewrite /base2rev bin_of_nate /= rev_cons - nat_of_list_rF. 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)