proposition: Lemma pcoreS pi gT (G H : {group gT}) : H \subset G -> H :&: 'O_pi(G) \subset 'O_pi(H).
proof: Proof. move=> sHG; rewrite -{2}(setIidPl sHG). by do 2!rewrite -(morphim_idm (subsetIl H _)) morphimIdom; apply: morphim_pcore. 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)