proposition: Lemma pos_of_bitseq_nseq_false : forall p, Pos.to_nat (pos_of_bitseq (nseq p false)) = 2 ^ p.
proof: Proof. elim=> // p IH /=; by rewrite expnS -IH Pos2Nat.inj_xO. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype tuple) BinPos BinNat PArith ssr_ext