proposition: Lemma pos_of_bitseq_up : forall p l, size l <= p -> Pos.to_nat (pos_of_bitseq l) < 2 ^ p.+1.
proof: Proof. elim=> [|p ih [|h t] //]; first by destruct l. - move=> _ /=. by rewrite (@leq_ltn_trans 1) // -{1}(expn0 2) ltn_exp2l. - move=> H1 /=. destruct h. rewrite Pos2Nat.inj_xI expnS multE. rewrite (@leq_trans (2 * (Pos.to_nat (pos_of_bitseq t)).+1)) //. by rewrite mulnS addnC addn2. by rewrite leq_mul2l /= ih. by rewrite Pos2Nat.inj_xO expnS multE ltn_mul2l /= ih. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype tuple) BinPos BinNat PArith ssr_ext