proposition: Lemma N_of_bitseq_0 : forall n0 p, N_of_bitseq p = N0 -> size p = n0 -> p = nseq n0 false.
proof: Proof. elim => [ [] // | n0 IH [|[] t] //= Hp [Hsz] ]. by rewrite -(IH t). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype tuple) BinPos BinNat PArith ssr_ext