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