proposition: Lemma bitseq_of_N_inj : injective bitseq_of_N.
proof: Proof. case. - by case => // a /= /esym/bitseq_of_pos_not_false. - move=> a /= [] //=. + by move/bitseq_of_pos_not_false. + by move=> b /bitseq_of_pos_inj ->. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype tuple) BinPos BinNat PArith ssr_ext