proposition: Lemma base2_rev_invert n: odd n -> n != 1 -> (base2rev n.-1) + bin_invert(base2rev n) = 2^(log2 n).
proof: Proof. move => on nn1; have eq1:= (oddE on). have pv: 2 ^ (log2 n).-1 = 2 ^ log2 n./2 by rewrite {1} eq1 log2_Sdouble succnK. move: (base2r_odd n./2); rewrite - eq1 - pv => eq2. case H: (base2rev n./2 == 0). move: eq2 nn1; rewrite {1 4} eq1 (eqP H) addn0 => sa. move:(odd_base2rev (n./2).*2); rewrite sa pv; case (n./2) => // q. by rewrite log2S_k expn2S odd_double. rewrite {1 3} eq1 log2S_k succnK base2rev_even -eq1 expnS. have: 2 ^ (log2 n).-1 < base2rev n. by rewrite eq2 - (@prednK (base2rev n./2)) ?lt0n ?H // addnS ltnS leq_addr. rewrite -(log_base2r on) => leq1; apply /eqP. rewrite -(eqn_add2l (base2rev n)) addnCA (bin_invert_p1 leq1). by rewrite (log_base2r on) mulSn addnA eqn_add2r addnC - eq2. 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)