proposition: Corollary cyclic_Sylow_tiVsub_der1 : cyclic S -> S :&: G^`(1) = 1 \/ S \subset G^`(1).
proof: Proof. move=> cycS; have [sSG pS _] := and3P sylS. have nsSN: S <| 'N_G(S) by rewrite normalSG. have hallSN: Hall 'N_G(S) S. by apply: pHall_Hall (pHall_subl _ _ sylS); rewrite ?subsetIl ?normal_sub. have /splitsP[K /complP[tiSK /= defN]] := SchurZassenhaus_split hallSN nsSN. have sKN: K \subset 'N_G(S) by rewrite -defN mulG_subr. have [sKG nSK] := subsetIP sKN. have coSK: coprime #|S| #|K|. by case/andP: hallSN => sSN; rewrite -divgS //= -defN TI_cardMg ?mulKn. have:= coprime_abelian_cent_dprod nSK coSK (cyclic_abelian cycS). case/(cyclic_pgroup_dprod_trivg pS cycS) => [[_ cSK]|[_ <-]]; last first. by right; rewrite commgSS. have cSN: 'N_G(S) \subset 'C(S). by rewrite -defN mulG_subG -abelianE cyclic_abelian // centsC -cSK subsetIr. have /sdprodP[_ /= defG _ _] := Burnside_normal_complement cSN. set Q := 'O_p^'(G) in defG; have nQG: G \subset 'N(Q) := gFnorm _ _. left; rewrite coprime_TIg ?(pnat_coprime pS) //. apply: pgroupS (pcore_pgroup _ G); rewrite /= -/Q. rewrite -quotient_sub1 ?gFsub_trans ?quotientR //= -/Q. rewrite -defG quotientMidl (sameP trivgP commG1P) -abelianE. by rewrite morphim_abelian ?cyclic_abelian. 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)