proposition: Lemma pad_seqL_inj n s t : size s = n -> size t = n -> pad_seqL s n = pad_seqL t n -> s = t.
proof: Proof. elim: n s t => [[] // [] // | ] n IH [|a' ta] // [|b tb] // [Ha] [Hb]. by rewrite /pad_seqL /= Ha Hb ltnS leqnn subnn. Qed.
imports: mathcomp(all_ssreflect fingroup perm)