proposition: Lemma bitseq_of_nat_expn2 p m : p < m -> bitseq_of_nat (2 ^ p) m = nseq (m - p.+1) false ++ true :: nseq p false.
proof: Proof. move=> pm. rewrite /bitseq_of_nat /= /pad_seqL /= bitseq_of_N_bin_of_nat_expn2 size_rev. by rewrite size_cat size_nseq /= -ltnS addn1 ltnS pm rev_cat /= rev_nseq. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype tuple) BinPos BinNat PArith ssr_ext