proposition: Lemma size_pad_seqL n s : size (pad_seqL s n) = n.
proof: Proof. rewrite /pad_seqL; case: ifPn; last by rewrite -ltnNge size_take => ->. by rewrite size_cat size_nseq => /subnK. Qed.
imports: mathcomp(all_ssreflect fingroup perm)