proposition: Lemma permuted_action_trans : [transitive [set: 'S_n], on [set: permuted w] | pact].
proof: Proof. Proof using. apply/imsetP; exists (Permuted (perm_refl w)); first by []. apply/setP => /= t; rewrite !inE; apply/esym/orbitP => /=. have:= permutedP t => /tuple_permP[s /val_inj Hs]. exists s; first by rewrite inE. apply val_inj => /=; apply eq_from_tnth => /= i. by rewrite {1}Hs !tnth_mktuple permKV. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup action gproduct) tools combclass sorted partition composition multinomial permcomp cycles