proposition: Lemma bitseq_of_pos_not_nseq_false i r : bitseq_of_pos i <> nseq r false.
proof: Proof. elim : i r => /= [p Hp [] //|| [] //]. move=> p Hp [] // r [X]. by apply Hp with r. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype tuple) BinPos BinNat PArith ssr_ext