proposition: Lemma uniq_mmax_subset1 U M : M \in 'M -> U \subset M -> (U \in 'U) = ('M(U) \subset [set M]).
proof: Proof. move=> maxM sUM; apply/idP/idP=> uU; first by rewrite -(def_uniq_mmax uU). by apply/uniq_mmaxP; exists M; apply/eqP; rewrite eqEsubset uU sub1set inE maxM. 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)