proposition: Lemma permutedact_is_action : is_action [set: 'S_n] permutedact.
proof: Proof. Proof using. split => /= [s t1 t2 Heq | t s1 s2 _ _]. - apply val_inj; apply eq_from_tnth => i. move: Heq => /(congr1 (fun t => tnth t (s i))). by rewrite !tnth_mktuple permK. - apply val_inj; apply eq_from_tnth => /= i. by rewrite !tnth_mktuple invMg permM. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup action gproduct) tools combclass sorted partition composition multinomial permcomp cycles