proposition: Lemma inporbits_im s : inporbits s @: 'C[s] = stab_iporbits s.
proof: Proof. Proof using. apply/setP => /= P; apply/imsetP/idP => /= [[/= x Hx ->] | HP]. - rewrite inE; apply/andP; split. + by rewrite inE; apply: restr_perm_on. + apply/bigcapP => [[i Hi] _] /=; apply/astabsP => X. have/actsP/(_ _ Hx X)/= := cent1_act_on_iporbits s i. rewrite !inE !apermE; case: (boolP (X \in porbits s)) => /= [HX| HX _]. * rewrite restr_permE // ?actpermE // {X HX}. apply/astabsP => X /=; rewrite apermE actpermE /=. exact: (actsP (cent1_act_on_porbits s)). * rewrite (out_perm (restr_perm_on _ _) HX). by move: HX => /negbTE ->. - by exists (permcycles s P); [apply: permcyclesP | rewrite permcyclesK]. 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