proposition: Lemma uniq_mmaxJ K x :((K :^ x)%G \in 'U) = (K \in 'U).
proof: Proof. apply/uniq_mmaxP/uniq_mmaxP=> [] [M uK_M]. by exists (M :^ x^-1)%G; rewrite -(conjsgK x K); apply: def_uniq_mmaxJ. by exists (M :^ x)%G; apply: def_uniq_mmaxJ. 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)