proposition: Lemma permcyclesM s : {in stab_iporbits s &, {morph permcycles s : P Q / P * Q}}.
proof: Proof. Proof using. move=> /= P Q HP HQ /=; apply/permP => X. rewrite permM !permE -[RHS]/((_ \o _) X). apply esym; apply cymap_comp => C HC /=. by rewrite groupM // HP HQ permM. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(tuple path bigop finset div) mathcomp(fingroup perm action gproduct morphism) tools partition permcomp cycles cycletype