proposition: Lemma size_bitseq_of_N_lb' : forall i n, 2 ^ n <= nat_of_bin i -> n < size (bitseq_of_N i).
proof: Proof. case => [m|]; first by rewrite leqn0 expn_eq0. elim => [p ih m K /= | p ih m K /= | m]. - case: m K => [//|m K]. have /ih : 2 ^ m <= nat_of_pos p. move: K. by rewrite /= NatTrec.doubleE expnS -ltnS -doubleS -muln2 mulnC ltn_pmul2r. by rewrite ltnS. - case: m K => [//|m K]. have /ih : 2 ^ m <= nat_of_pos p. by rewrite /= NatTrec.doubleE expnS -muln2 mulnC leq_pmul2r in K. by rewrite ltnS. - by rewrite -[in X in _ <= X](_ : 2 ^ 0 = 1%num) // leq_exp2l. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype tuple) BinPos BinNat PArith ssr_ext