proposition: Lemma mmax_neq1 M : M \in 'M -> M :!=: 1.
proof: Proof. move=> maxM; apply: contra mFT_nonAbelian; move/eqP=> M1. case: (eqVneq G 1) => [-> | ]; first exact: abelian1. case/trivgPn=> x; rewrite -cycle_subG -cycle_eq1 subEproper /=. case/predU1P=> [<- | ]; first by rewrite cycle_abelian. by move/(mmax_max maxM)=> ->; rewrite M1 ?sub1G ?eqxx. Qed.
imports: HB(structures) mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq div choice fintype bigop) mathcomp(finset prime fingroup morphism automorphism action quotient) mathcomp(gfunctor cyclic pgroup center commutator gseries nilpotent) mathcomp(sylow abelian maximal hall) odd_order(BGsection1 BGsection6)