proposition: Lemma log2_bin_invert n: log2(bin_invert n) = log2 n.
proof: Proof. rewrite /bin_invert /log2 nat_of_binK num_of_list_sizeK. case: (list_of_num (bin_of_nat n)) => // a l; elim: l a; first by case. by move => a l H; case; [ rewrite /= size_map | move: (H a); move => /= ->]. 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)