proposition: Lemma FTtypeP_pair_witness : exists2 T, typeP_pair M T defW & exists xdefW : W2 \x W1 = W, exists V : {group gT}, of_typeP T V xdefW.
proof: Proof. have Mtype'1 := FTtypeP_neq1 maxM MtypeP. case: FTtypeP_pair_cases => [/(_ M maxM)/idPn[] // | [S [T]]]. case=> _ Wx W1x W2x defWx pairST. without loss /imsetP[y2 _ defSy]: S T W1x W2x defWx pairST / gval M \in S :^: G. have [_ _ _ _ coverST] := pairST => IH. have /setUP[] := coverST M maxM Mtype'1; first exact: IH pairST. by apply: IH (typeP_pair_sym _ pairST); rewrite dprodC. have [U_S StypeP] := typeP_pairW pairST. have [[_ maxS maxT] [defS defT defST] b2 b3 b4] := pairST. have [[[_ _ _ defM] _ _ _ _] defW2] := (MtypeP, typeP_cent_compl MtypeP). have /imsetP[y1 Sy1 /(canRL (conjsgKV _)) defW1]: W1 :^ y2^-1 \in W1x :^: S. apply: (of_typeP_compl_conj StypeP). by rewrite -(conjsgK y2 S) -defSy derJ -sdprodJ defM. pose y := (y1 * y2)%g; rewrite -conjsgM -/y in defW1. have{} defSy: S :^ y = M by rewrite conjsgM (conjGid Sy1). have{} defW2: W2 :=: W2x :^ y. by rewrite -(typeP_cent_compl StypeP) conjIg -derJ -centJ defSy -defW1. suffices pairMTy: typeP_pair M (T :^ y) defW. exists (T :^ y)%G => //; have xdefW: W2 \x W1 = W by rewrite dprodC. by exists xdefW; apply: typeP_pairW (typeP_pair_sym xdefW pairMTy). do [split; rewrite ?defM -?defSy ?mmaxJ ?FTtypeJ //] => [|L maxL /(b4 L maxL)]. by rewrite -defW defW1 defW2 derJ -sdprodJ -dprodJ -conjIg defT defST defWx. by rewrite !conjugates_conj lcoset_id // inE. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq path div choice) mathcomp(fintype tuple finfun bigop prime ssralg poly finset center) mathcomp(fingroup morphism perm automorphism quotient action finalg zmodp) mathcomp(gfunctor gproduct cyclic commutator nilpotent pgroup) mathcomp(sylow hall abelian maximal frobenius) mathcomp(matrix mxalgebra mxrepresentation vector) odd_order(BGsection1 BGsection3 BGsection7 BGsection10) odd_order(BGsection14 BGsection15 BGsection16) mathcomp(algC classfun character inertia vcharacter) odd_order(PFsection1 PFsection2 PFsection3 PFsection4 PFsection5)