proposition: Lemma pcoreI pi rho G : 'O_[predI pi & rho](G) = 'O_pi('O_rho(G)).
proof: Proof. apply/eqP; rewrite eqEsubset !pcore_max //. - rewrite /pgroup pnatI -!pgroupE. by rewrite pcore_pgroup (pgroupS (pcore_sub pi _))// pcore_pgroup. - by rewrite !gFnormal_trans. - by apply: sub_pgroup (pcore_pgroup _ _) => p /andP[]. apply/andP; split; first by apply: sub_pcore => p /andP[]. by rewrite gFnorm_trans ?normsG ?gFsub. 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)