proposition: Proposition coprime_comm_pcore A G K : A \subset 'N(G) -> coprime #|G| #|A| -> solvable G -> pi^'.-Hall(G) K -> K \subset 'C_G(A) -> [~: G, A] \subset 'O_pi(G).
proof: Proof. move=> nGA coGA solG hallK cKA. case: (coprime_Hall_exists nGA) => // H hallH nHA. have sHG: H \subset G by case/andP: hallH. have sKG: K \subset G by case/andP: hallK. have coKH: coprime #|K| #|H|. case/and3P: hallH=> _ piH _; case/and3P: hallK => _ pi'K _. by rewrite coprime_sym (pnat_coprime piH pi'K). have defG: G :=: K * H. apply/eqP; rewrite eq_sym eqEcard coprime_cardMg //. rewrite -{1}(mulGid G) mulgSS //= (card_Hall hallH) (card_Hall hallK). by rewrite mulnC partnC. have sGA_H: [~: G, A] \subset H. rewrite gen_subG defG. apply/subsetP=> _ /imset2P[_ a /imset2P[x y Kx Hy ->] Aa ->]. rewrite commMgJ (([~ x, a] =P 1) _) ?(conj1g, mul1g). by rewrite groupMl ?groupV // memJ_norm ?(subsetP nHA). by rewrite subsetI sKG in cKA; apply/commgP/(centsP cKA). apply: pcore_max; last first. by rewrite /(_ <| G) /= commg_norml commGC commg_subr nGA. by case/and3P: hallH => _ piH _; apply: pgroupS piH. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div choice) mathcomp(fintype finset prime fingroup morphism) mathcomp(automorphism quotient action gproduct gfunctor) mathcomp(commutator center pgroup finmodule nilpotent) mathcomp(sylow abelian maximal)