proposition: Corollary Zgroup_der1_Hall gT (G : {group gT}) : Zgroup G -> Hall G G^`(1).
proof: Proof. move=> ZgG; set G' := G^`(1). rewrite /Hall der_sub coprime_sym coprime_pi' ?cardG_gt0 //=. apply/pgroupP=> p p_pr pG'; have [P sylP] := Sylow_exists p G. have cycP: cyclic P by have:= forallP ZgG P; rewrite (p_Sylow sylP). case: (cyclic_Sylow_tiVsub_der1 sylP cycP) => [tiPG' | sPG']. have: p.-Sylow(G') (P :&: G'). by rewrite setIC (Sylow_setI_normal _ sylP) ?gFnormal. move/card_Hall/eqP; rewrite /= tiPG' cards1 eq_sym. by rewrite partn_eq1 ?cardG_gt0 // p'natE ?pG'. rewrite inE /= mem_primes p_pr indexg_gt0 -?p'natE // -partn_eq1 //. have sylPq: p.-Sylow(G / G') (P / G') by rewrite morphim_pHall ?normsG. rewrite -card_quotient ?gFnorm // -(card_Hall sylPq) -trivg_card1. by rewrite /= -quotientMidr mulSGid ?trivg_quotient. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq path div fintype) mathcomp(bigop prime binomial finset fingroup morphism perm automorphism) mathcomp(quotient action gproduct gfunctor commutator) mathcomp(ssralg finalg zmodp cyclic center pgroup finmodule gseries) mathcomp(nilpotent sylow abelian maximal hall extremal) mathcomp(matrix mxalgebra mxrepresentation mxabelem)