proposition: Lemma cent1_act_porbit s t x : t \in 'C[s] -> ('P)^* (porbit s x) t = porbit s (t x).
proof: Proof. Proof using. move=> /cent1P Hcom. apply/setP => y; apply/imsetP/porbitP. - move=> [z /porbitP[i ->{z}] ->{y}]. by exists i => /=; rewrite -!permM (commuteX i Hcom) permM. - move=> [i ->{y}]. exists ((s ^+ i) x); first exact: mem_porbit. by rewrite -!permM (commuteX i Hcom) 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