proposition: Lemma bigcap_p'core pi G : G :&: \bigcap_(p < #|G|.+1 | (p : nat) \in pi) 'O_p^'(G) = 'O_pi^'(G).
proof: Proof. apply/eqP; rewrite eqEsubset subsetI pcore_sub pcore_max /=. - by apply/bigcapsP=> p pi_p; apply: sub_pcore => r; apply: contraNneq => ->. - apply/pgroupP=> q q_pr qGpi'; apply: contraL (eqxx q) => /= pi_q. apply: (pgroupP (pcore_pgroup q^' G)) => //. have qG: q %| #|G| by rewrite (dvdn_trans qGpi') // cardSg ?subsetIl. have ltqG: q < #|G|.+1 by rewrite ltnS dvdn_leq. rewrite (dvdn_trans qGpi') ?cardSg ?subIset //= orbC. by rewrite (bigcap_inf (Ordinal ltqG)). rewrite /normal subsetIl normsI ?normG // norms_bigcap //. by apply/bigcapsP => p _; apply: gFnorm. 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)