proposition: Lemma mmax_normal_subset A M : M \in 'M -> A <| M -> ~~ (A \subset [1]) -> 'N(A) = M.
proof: Proof. rewrite -gen_subG subG1 => maxM /andP[sAM nAM] ntGA. rewrite (mmax_max maxM) // (sub_proper_trans (norm_gen _)) ?mFT_norm_proper //. by rewrite (sub_mmax_proper maxM) // gen_subG. 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)