proposition: Lemma SCN_max A : A \in 'SCN(G) -> [max A | A <| G & abelian A].
proof: Proof. case/SCN_P => nAG scA; apply/maxgroupP; split=> [|H]. by rewrite nAG /abelian -{1}scA subsetIr. do 2![case/andP]=> sHG _ abelH sAH; apply/eqP. by rewrite eqEsubset sAH -scA subsetI sHG centsC (subset_trans sAH). 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)