proposition: Lemma cent1_act_on_iporbits s i : [acts 'C[s], on porbits s :&: 'SC_i | ('P)^*].
proof: Proof. Proof using. apply/subsetP => t Ht; apply (subsetP (astabsI _ _ _)). rewrite inE (subsetP (cent1_act_on_porbits s)) //=. rewrite /astabs !inE /=; apply/subsetP => P; rewrite !inE. by rewrite card_setact. 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