proposition: Lemma max_SCN A : p.-group G -> [max A | A <| G & abelian A] -> A \in 'SCN(G).
proof: Proof. move/pgroup_nil=> nilG; rewrite /abelian. case/maxgroupP=> /andP[nsAG abelA] maxA; have [sAG nAG] := andP nsAG. rewrite inE nsAG eqEsubset /= andbC subsetI abelA normal_sub //=. rewrite -quotient_sub1; last by rewrite subIset 1?normal_norm. apply/trivgP; apply: (TI_center_nil (quotient_nil A nilG)). by rewrite quotient_normal // /normal subsetIl normsI ?normG ?norms_cent. apply/trivgP/subsetP=> _ /setIP[/morphimP[x Nx /setIP[_ Cx]] ->]. rewrite -cycle_subG in Cx => /setIP[GAx CAx]. have{CAx GAx}: <[coset A x]> <| G / A. by rewrite /normal cycle_subG GAx cents_norm // centsC cycle_subG. case/(inv_quotientN nsAG)=> B /= defB sAB nBG. rewrite -cycle_subG defB (maxA B) ?trivg_quotient // nBG. have{} defB : B :=: A * <[x]>. rewrite -quotientK ?cycle_subG ?quotient_cycle // defB quotientGK //. exact: normalS (normal_sub nBG) nsAG. apply/setIidPl; rewrite ?defB -[_ :&: _]center_prod //=. rewrite /center !(setIidPl _) //; apply: cycle_abelian. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(div fintype finfun bigop finset prime binomial) mathcomp(fingroup morphism perm automorphism quotient) mathcomp(action commutator gproduct gfunctor ssralg) mathcomp(countalg finalg zmodp cyclic pgroup center gseries) mathcomp(nilpotent sylow abelian finmodule)