proposition: Lemma size_pad_positive c (s : bitseq) : pad_seqL false (rev (c :: bitseq_of_pos (pos_of_bitseq s))) (size s).+2 = rcons (pad_seqL false (rev (bitseq_of_pos (pos_of_bitseq s))) (size s).+1) c.
proof: Proof. rewrite /pad_seqL !size_rev /= ltnS. case: ifPn => Hsz; first by rewrite subSS rev_cons rcons_cat. have Hup := pos_of_bitseq_up (leqnn (size s)). have Hub' := @size_bitseq_of_N_ub' (Npos (pos_of_bitseq s)) (size s).+1 (@nat_of_pos_not_0 _). rewrite /= -BinPos_nat_of_P_nat_of_pos in Hub'. by rewrite Hub' in Hsz. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype tuple) BinPos BinNat PArith ssr_ext