proposition: Lemma bitseq_of_nat_0 n : bitseq_of_nat 0 n = nseq n false.
proof: Proof. rewrite /bitseq_of_nat /= /pad_seqL /=. case: ifP => [Hn|]; last by case: n. by rewrite cats1 -nseq_S subn1 prednK. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype tuple) BinPos BinNat PArith ssr_ext