proposition: Lemma permutedact_subproof t (s : 'S_n) : perm_eq w [tuple tnth t (s^-1 i) | i < n].
proof: Proof. Proof using. apply: (perm_trans (permutedP t)). by rewrite /= perm_sym; apply/tuple_permP; exists s^-1. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup action gproduct) tools combclass sorted partition composition multinomial permcomp cycles