proposition: Lemma Npos_pos_of_bitseq_rev x y : rev (bitseq_of_N (bin_of_nat x)) = true :: y -> Npos (pos_of_bitseq (rev y)) = x :> nat.
proof: Proof. move=> H. by rewrite (@Npos_pos_of_bitseq_rev' (bin_of_nat x) y H) bin_of_natK. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype tuple) BinPos BinNat PArith ssr_ext