proposition: Lemma size_N_of_bitseqK (s : bitseq) : size s > 0 -> size (bitseq_of_N (bin_of_nat (N_of_bitseq s))) <= size s.
proof: Proof. move=> Hs. case Hbs : (bin_of_nat _) => //. apply size_bitseq_of_N_ub'. by apply nat_of_pos_not_0. by rewrite -Hbs bin_of_natK -Nto_natE N_of_bitseq_up. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype tuple) BinPos BinNat PArith ssr_ext