proposition: Lemma conj_porbitgrp s y z : y \in 'C[s] -> z \in 'CC(s) -> z ^ y \in 'CC(s).
proof: Proof. Proof using. move=> Hy; rewrite inE => /andP[zC /astabP zCporbits]. have /= HyV := groupVr Hy. rewrite inE; apply/andP; split. - by apply groupM; last exact: groupM. - apply/astabP => C /imsetP[x _ ->{C}]. rewrite !actM /= cent1_act_porbit // zCporbits; last exact: imset_f. by rewrite -cent1_act_porbit // -!actM mulVg act1. 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