proposition: Lemma cent1_act_on_porbits s : [acts 'C[s], on porbits s | ('P)^*].
proof: Proof. Proof using. apply/subsetP => t Hcent; rewrite /astabs !inE /=. apply/subsetP => C; rewrite inE => /imsetP[x _ ->{C}]. by apply/imsetP; exists (t x); [| apply: cent1_act_porbit]. 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