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