proposition: Lemma base2r_odd n: base2rev (n.*2.+1) = 2^ (log2 n) + base2rev n.
proof: Proof. case: n => // n; rewrite /base2rev /log2 bin_of_nato /= rev_cons - size_rev. by elim: (rev _) => // a l /= ->; rewrite doubleD -expn2S -addnS; case: a. 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)