proposition: Lemma prime_nil_der1_factor G : nilpotent G^`(1) -> prime #|G / G^`(1)| -> Hall G G^`(1) /\ (forall H, G^`(1) ><| H = G -> G^`(1) = [~: G, H]).
proof: Proof. move=> nilG' /=; set G' := G^`(1); set p := #|G / G'| => p_pr. have nsG'G: G' <| G := der_normal 1 G; have [sG'G nG'G] := andP nsG'G. have nsG'p'G: 'O_p^'(G') <| G := gFnormal_trans _ nsG'G. have nG'p'G := normal_norm nsG'p'G; have solG' := nilpotent_sol nilG'. have{nilG'} pGb: p.-group (G / 'O_p^'(G')). rewrite /pgroup card_quotient -?(Lagrange_index sG'G (pcore_sub _ _)) //=. rewrite pnatM // -card_quotient // pnat_id //= -pnatNK. by case/and3P: (nilpotent_pcore_Hall p^' nilG'). have{pGb} cycGb: cyclic (G / 'O_p^'(G')). apply: (cyclic_nilpotent_quo_der1_cyclic (pgroup_nil pGb)). rewrite -quotient_der // (isog_cyclic (third_isog _ _ _)) ?pcore_sub //. by apply: prime_cyclic. have defG': G' = 'O_p^'(G'). by apply/eqP; rewrite eqEsubset pcore_sub der1_min ?cyclic_abelian. have hallG': Hall G G'. rewrite /Hall sG'G -?card_quotient // defG' //= -/p. by rewrite (p'nat_coprime (pcore_pgroup _ _)) ?pnat_id. split=> // H defG; have [_ mulG'H nG'H tiG'H] := sdprodP defG. rewrite -mulG'H commMG ?commg_normr // -derg1 (derG1P _) ?mulg1 //. by case/coprime_der1_sdprod: (defG); rewrite ?(coprime_sdprod_Hall_l defG). rewrite (isog_abelian (quotient_isog nG'H tiG'H)) /= -/G'. by rewrite -quotientMidl mulG'H der_abelian. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq div fintype finset) mathcomp(prime fingroup morphism automorphism quotient gproduct gfunctor) mathcomp(cyclic center commutator pgroup nilpotent sylow abelian hall) mathcomp(maximal) odd_order(BGsection1 BGappendixAB)