proposition: Lemma log2_bnd n (k := log2 n.+1): 2^(k.-1) <= n.+1 < 2^k.
proof: Proof. move /ends_with_aP:(nat_list_succ' n) => [w /= eq]. rewrite /k /log2 /= eq -(bin_of_natK n.+1) -(list_of_numK (_ n.+1)) /= eq. rewrite size_rcons succnK; move: (w); clear; elim => // a l. rewrite rcons_cons;case: (rcons l true). by rewrite /= leqn0 !expnS => /andP [/eqP ->]. move => b l'; set q := nat_of_bin _; set q' := nat_of_bin _. have -> : q' = if a then q.*2.+1 else q.*2. by rewrite /q/q' /=; case: (a);rewrite /= natTrecE. rewrite /= !expn2S;case: (a). by rewrite leq_Sdouble ltn_Sdouble. by rewrite leq_double ltn_double. 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)