proposition: Lemma Npos_pos_of_bitseq_rev' : forall x y, rev (bitseq_of_N x) = true :: y -> Npos (pos_of_bitseq (rev y)) = nat_of_bin x :> nat.
proof: Proof. elim/Nind => // x IH y. move Heq : (N.succ x) => eq. destruct eq => //= H. f_equal. by apply pos_of_bitseq_rev in H. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype tuple) BinPos BinNat PArith ssr_ext