proposition: Lemma N_of_bitseq_bitseq_of_nat m x : x <> O -> (x < 2 ^ m)%nat -> N_of_bitseq (bitseq_of_nat x m) = x :> nat.
proof: Proof. move=> Hx x_m. rewrite /N_of_bitseq /bitseq_of_nat. have Hx' : bin_of_nat x <> N0. contradict Hx. rewrite (_ : 0 = bin_of_nat (nat_of_bin 0))%N // in Hx. by apply bin_of_nat_inj in Hx. case: (@bitseq_of_N_leading_bit _ Hx') => y Hy. rewrite Hy. rewrite rem_lea_false_pad_seqL; last first. move: (size_bitseq_of_N_ub Hx x_m). by rewrite -size_rev Hy. by apply Npos_pos_of_bitseq_rev in Hy. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype tuple) BinPos BinNat PArith ssr_ext