proposition: Lemma perm_tuple_comp n (s1 s2 : 'S_n) (t : n.-tuple A) : perm_tuple s1 (perm_tuple s2 t) = perm_tuple (s1 * s2) t.
proof: Proof. apply eq_from_tnth => i. by rewrite /perm_tuple !tnth_map /= tnth_ord_tuple permM. Qed.
imports: mathcomp(all_ssreflect fingroup perm)