proposition: Lemma nilpotent_pcoreC pi G : nilpotent G -> 'O_pi(G) \x 'O_pi^'(G) = G.
proof: Proof. move=> nilG; have trO: 'O_pi(G) :&: 'O_pi^'(G) = 1. by apply: coprime_TIg; apply: (@pnat_coprime pi); apply: pcore_pgroup. rewrite dprodE //. apply/eqP; rewrite eqEcard mul_subG ?pcore_sub // (TI_cardMg trO). by rewrite !(card_Hall (nilpotent_pcore_Hall _ _)) // partnC ?leqnn. rewrite (sameP commG1P trivgP) -trO subsetI commg_subl commg_subr. by rewrite !gFsub_trans ?gFnorm. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(fintype prime bigop finset fingroup morphism) mathcomp(automorphism quotient action cyclic gproduct) mathcomp(gfunctor commutator pgroup center nilpotent)