proposition: Lemma pcore_modp pi gT (G H : {group gT}) : H <| G -> pi.-group H -> pcore_mod G pi H = 'O_pi(G).
proof: Proof. move=> nsHG piH; have nHG := normal_norm nsHG; apply/eqP. rewrite eqEsubset andbC -sub_morphim_pre ?(gFsub_trans, morphim_pcore) //=. rewrite -[G in 'O_pi(G)](quotientGK nsHG) pcore_max //. by rewrite -(pquotient_pgroup piH) ?subsetIl // cosetpreK pcore_pgroup. by rewrite morphpre_normal ?gFnormal ?gFsub_trans ?morphim_sub. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(fintype bigop finset prime fingroup morphism) mathcomp(gfunctor automorphism quotient action gproduct) mathcomp(cyclic)