proposition: Lemma def_uniq_mmax U M : U \in 'U -> M \in 'M -> U \subset M -> 'M(U) = [set M].
proof: Proof. case/uniq_mmaxP=> D uU_D maxM sUM. by rewrite (group_inj (eq_uniq_mmax uU_D maxM sUM)). 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)