proposition: Lemma sub_uniq_mmax U M H : 'M(U) = [set M] -> U \subset H -> H \proper G -> H \subset M.
proof: Proof. move=> uU_M sUH; case/mmax_exists=> D; case/setIdP=> maxD sHD. by rewrite -(eq_uniq_mmax uU_M maxD) ?(subset_trans sUH). 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)