proposition: Lemma uniq_mmax_neq1 (U : {group gT}) : U \in 'U -> U :!=: 1.
proof: Proof. case/uniq_mmaxP=> M uU_M; have [maxM _] := mem_uniq_mmax uU_M. apply: contraL (uniq_mmax_norm_sub uU_M); move/eqP->. by rewrite norm1 subTset -properT mmax_proper. 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)