proposition: Lemma N_of_bitseq_up : forall p l, size l <= p -> N.to_nat (N_of_bitseq l) < 2 ^ p.
proof: Proof. elim=> [[|//] _ /= |p IH [/=|h t]]. - by rewrite expn_gt0. - by rewrite expn_gt0. - rewrite /= ltnS => tp. destruct h; first by rewrite /= pos_of_bitseq_up // size_rev. by rewrite N_of_bitseq_false (ltn_trans (IH _ tp)) // ltn_exp2l. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype tuple) BinPos BinNat PArith ssr_ext