proposition: Lemma bitseq_of_N_nseq_false i r : i <> O -> bitseq_of_N (bin_of_nat i) <> nseq r false.
proof: Proof. case: i r => // i r _ /=; exact: bitseq_of_pos_not_nseq_false. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype tuple) BinPos BinNat PArith ssr_ext