proposition: Corollary P1type_trans : {in 'M_'P1 &, forall M H, gval H \in M :^: G}.
proof: Proof. move=> M H P1maxM P1maxH; have [PmaxM _] := setIdP P1maxM. have [[maxM _] [PmaxH _]] := (setDP PmaxM, setIdP P1maxH). have [K hallK] := Hall_exists \kappa(M) (mmax_sol maxM). have [Mstar _ [_ _ _ _ [_ [|]]]] := Ptype_embedding PmaxM hallK. by case; rewrite inE P1maxM. case=> /setDP[_ /negP notP1maxMstar] _. case/(_ H PmaxH)/setUP=> // /imsetP[a _ /group_inj defH]. by rewrite defH P1typeJ in P1maxH. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq div path fintype bigop order) mathcomp(finset prime fingroup morphism perm automorphism quotient) mathcomp(action gproduct gfunctor pgroup cyclic center commutator) mathcomp(gseries nilpotent sylow abelian maximal hall frobenius) mathcomp(ssralg ssrnum ssrint rat) odd_order(BGsection1 BGsection3 BGsection4 BGsection5 BGsection6) odd_order(BGsection7 BGsection9 BGsection10 BGsection12 BGsection13)