proposition: Lemma cyclic_pdiv_normal_complement gT (S G : {group gT}) : (pdiv #|G|).-Sylow(G) S -> cyclic S -> exists H : {group gT}, H ><| S = G.
proof: Proof. set p := pdiv _ => sylS cycS; have cSS := cyclic_abelian cycS. exists 'O_p^'(G)%G; apply: Burnside_normal_complement => //. have [-> | ntS] := eqsVneq S 1; first apply: cents1. have [sSG pS p'iSG] := and3P sylS; have [pr_p _ _] := pgroup_pdiv pS ntS. rewrite -['C(S)]mulg1 -ker_conj_aut -morphimSK ?subsetIr // setIC morphimIdom. set A_G := _ @* _; pose A := Aut S. have [_ [_ [cAA _ oAp' _]] _] := cyclic_pgroup_Aut_structure pS cycS ntS. have{cAA cSS p'iSG} /setIidPl <-: A_G \subset 'O_p^'(A). rewrite pcore_max -?sub_abelian_normal ?Aut_conj_aut //=. apply: pnat_dvd p'iSG; rewrite card_morphim ker_conj_aut /= setIC. have sSN: S \subset 'N_G(S) by rewrite subsetI sSG normG. by apply: dvdn_trans (indexSg sSN (subsetIl G 'N(S))); apply: indexgS. rewrite coprime_TIg ?sub1G // coprime_morphl // coprime_sym coprime_pi' //. apply/pgroupP=> q pr_q q_dv_G; rewrite !inE mem_primes gtnNdvd ?andbF // oAp'. by rewrite prednK ?prime_gt0 ?pdiv_min_dvd ?prime_gt1. 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)