proposition: Lemma sub_pcore pi rho G : {subset pi <= rho} -> 'O_pi(G) \subset 'O_rho(G).
proof: Proof. by move=> pi_sub_rho; apply: sub_in_pcore (in1W 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)