proposition: Lemma N_of_bitseqK (s : bitseq) : size s > 0 -> bitseq_of_nat (N.to_nat (N_of_bitseq s)) (size s) = s.
proof: Proof. clear. rewrite Nto_natE. elim: s => // b s IHs Hs /=. case b; simpl. rewrite /bitseq_of_nat nat_of_posK /=. rewrite -size_rev -{3}(revK s). elim: (rev s) => //. clear. move => b s IHs /=. rewrite -(cat1s b) rev_cat -cat_cons -IHs cats1. by case b; apply size_pad_positive. case Hs': (size s > 0); last by destruct s. rewrite -{3}IHs /bitseq_of_nat //. rewrite (_ : N_of_bitseq (false :: s) = N_of_bitseq s) //. rewrite /pad_seqL size_rev. have Hsz := size_N_of_bitseqK Hs'. rewrite !ifT //. by rewrite subSn. by apply leqW. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype tuple) BinPos BinNat PArith ssr_ext