proposition: Lemma restr_perm_genC C s t : C \in porbit_set s -> t \in 'CC(s) -> restr_perm C t \in <[restr_perm C s]>%G.
proof: Proof. Proof using. move=> HC; rewrite inE => /andP[/cent1P Hcomm /astabP Hstab]. apply/cycleP; apply commute_cyclic. - have: restr_perm C s \in cycle_dec s by apply/imsetP; exists C. by move/cyclic_dec. - apply/cent1P; rewrite /commute. have HS := porbit_set_astabs HC. have Ht : t \in 'N(C | 'P). rewrite -astab1_set; apply/astab1P; apply Hstab. by move: HC; rewrite inE => /andP[]. rewrite -((morphM (restr_perm_morphism C)) t s) //. rewrite -((morphM (restr_perm_morphism C)) s t) //. by rewrite Hcomm. - rewrite psupport_perm_on (psupport_restr_perm HC). exact: psupport_restr_perm_incl. 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