proposition: Lemma sub_in_pcore pi rho G : {in \pi(G), {subset pi <= rho}} -> 'O_pi(G) \subset 'O_rho(G).
proof: Proof. move=> pi_sub_rho; rewrite pcore_max ?pcore_normal //. apply: sub_in_pnat (pcore_pgroup _ _) => p. by move/(piSg (pcore_sub _ _)); apply: pi_sub_rho. 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)