proposition: Lemma def_uniq_mmaxS M U V : U \subset V -> V \proper G -> 'M(U) = [set M] -> 'M(V) = [set M].
proof: Proof. move=> sUV prV uU_M; apply/eqP; rewrite eqEsubset sub1set -uU_M. rewrite mmax_ofS //= inE (sub_uniq_mmax uU_M) //. by case/mem_uniq_mmax: 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)