proposition: Lemma mmax_norm_notJ M Mstar p X : M \in 'M -> Mstar \in 'M -> p.-group X -> X \subset M -> 'N(X) \subset Mstar -> [|| [&& p \in \sigma(M) & M :!=: Mstar], p \in \tau1(M) | p \in \tau3(M)] -> gval Mstar \notin M :^: G.
proof: Proof. move: Mstar => H maxM maxH pX sXM sNH; apply: contraL => MG_H. have [x Gx defH] := imsetP MG_H. have [sMp | sM'p] := boolP (p \in \sigma(M)); last first. have:= prime_class_mmax_norm maxH pX sNH. rewrite defH /= sigmaJ tau2J !negb_or (negPf sM'p) /= => t2Mp. by rewrite (contraL (@tau2'1 _ p)) // [~~ _]tau3'2. rewrite !(sMp, inE) orbF negbK. have [_ transCX _] := sigma_group_trans maxM sMp pX. set maxMX := finset _ in transCX. have maxMX_H: gval H \in maxMX by rewrite inE MG_H (subset_trans (normG X)). have maxMX_M: gval M \in maxMX by rewrite inE orbit_refl. have [y cXy ->] := atransP2 transCX maxMX_H maxMX_M. by rewrite /= conjGid // (subsetP sNH) // (subsetP (cent_sub X)). Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq choice div fintype) mathcomp(path bigop finset prime fingroup morphism perm automorphism) mathcomp(quotient action gproduct gfunctor pgroup cyclic commutator) mathcomp(center gseries nilpotent sylow abelian maximal hall frobenius) odd_order(BGsection1 BGsection3 BGsection4 BGsection5 BGsection6) odd_order(BGsection7 BGsection9 BGsection10 BGsection11)