proposition: Lemma norm_mmax M : M \in 'M -> 'N(M) = M.
proof: Proof. move=> maxM; apply: mmax_max (normG M) => //. exact: (mFT_norm_proper (mmax_neq1 maxM) (mmax_proper maxM)). 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)