proposition: Lemma mmax_ofS H K : H \subset K -> 'M(K) \subset 'M(H).
proof: Proof. move=> sHK; apply/subsetP=> M; rewrite !inE => /andP[->]. exact: subset_trans. 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)