proposition: Lemma log_base2r n: odd n -> log2 (base2rev n) = log2 n.
proof: Proof. suff H: forall m, odd m -> log2 m <= log2 (base2rev m). move => on;move: (H _ on) (H _ (odd_base2rev n.-1)). have ->: n.-1.+1 = n by move: on; case n. by rewrite (base2rev_oddI on) =>sa sb; apply /eqP; rewrite eqn_leq sa sb. move => m on; rewrite (oddE on) base2r_odd log2_Sdouble. by case:m./2 => // m1; rewrite - log2_pow; apply:leqn_log; apply leq_addr. 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)