proposition: Lemma rfd_morph : {in 'C_('Sym_T)[x | 'P] &, {morph rfd : y z / y * z}}.
proof: Proof. move=> p q; rewrite !setIA !setIid; move/astab1P=> p_x; move/astab1P=> q_x. apply/permP=> u; apply: val_inj. by rewrite permE /= !permM !permE /= [p x]p_x [q x]q_x eqxx permM /=. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(div fintype tuple tuple bigop prime finset fingroup) mathcomp(morphism perm automorphism quotient action cyclic) mathcomp(pgroup gseries sylow primitive_action)