proposition: Lemma permcyclesK s : {in stab_iporbits s, cancel (permcycles s) (inporbits s)}.
proof: Proof. Proof using. move=> /= P HP; apply/permP => /= C. rewrite /inporbits /=. case: (boolP (C \in porbits s)) => HC. - rewrite !restr_permE // ?actpermE /=; first last. apply/astabsP => {HC} C; rewrite /= apermE actpermE /=. apply (actsP (cent1_act_on_porbits s)). exact: permcyclesP. move: HC => /imsetP[x _ ->{C}]. rewrite cent1_act_porbit; last exact: permcyclesP. exact: porbit_permcycles. - rewrite (out_perm (restr_perm_on _ _) HC). by move: HP; rewrite inE => /andP[]; rewrite inE => /out_perm ->. 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