proposition: Lemma tuple2N_0 n : forall p, tuple2N p = N0 -> p = [tuple of nseq n false].
proof: Proof. case=> p Hp /= Hp'. apply val_inj => /=. apply N_of_bitseq_0 => //; by apply/eqP. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype tuple) BinPos BinNat PArith ssr_ext