proposition: Lemma max_normed_exists A X : pi.-group X -> A \subset 'N(X) -> {Y | Y \in |/|*(A; pi) & X \subset Y}.
proof: Proof. move=> piX nXA; pose piAn Y := pi.-group(Y) && (A \subset 'N(Y)). have [|Y] := @maxgroup_exists _ piAn X; first by rewrite /piAn piX. by exists Y; rewrite // inE. 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)