proposition: Lemma uniq_mmaxS U V : U \subset V -> V \proper G -> U \in 'U -> V \in 'U.
proof: Proof. move=> sUV prV /uniq_mmaxP[M uU_M]; apply/uniq_mmaxP; exists M. exact: def_uniq_mmaxS uU_M. 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)