proposition: Lemma eq_mmax : {in 'M &, forall M H, M \subset H -> M :=: H}.
proof: Proof. by move=> M H Mmax; move/mmax_proper=> prH; move/mmax_max->. 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)