proposition: Lemma uniq_mmax_norm_sub (M U : {group gT}) : 'M(U) = [set M] -> 'N(U) \subset M.
proof: Proof. move=> uU_M; have [maxM _] := mem_uniq_mmax uU_M. apply/subsetP=> x nUx; rewrite -(norm_mmax maxM) inE. have:= set11 M; rewrite -uU_M -(mmax_ofJ _ x) (normP nUx) uU_M. by move/set1P/congr_group->. 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)