proposition: Lemma of_typeP_pair (xdefW : W2 \x W1 = W) T V : T \in 'M -> of_typeP T V xdefW -> typeP_pair M T defW.
proof: Proof. have [S pairMS [xdefW' [V1 StypeP]]] := FTtypeP_pair_witness => maxT TtypeP. have [[cycW2 /andP[sW2T _] ntW2 _] _ _ [cycW1 _ _ sW1T'' _] _] := TtypeP. have{sW1T'' sW2T} sWT: W \subset T. by rewrite -(dprodW defW) mul_subG ?(subset_trans sW1T'') ?gFsub. have [cycW _ /and3P[_ _ /eqP defNW]] := ctiW. rewrite (@group_inj _ T S) //; have{pairMS} [_ _ _ _ defT] := pairMS. have /defT/setUP[] := FTtypeP_neq1 maxT TtypeP => {defT}// /imsetP[x _ defT]. have [defWx] := conj_of_typeP MtypeP x; rewrite -defT. case/(of_typeP_conj TtypeP)=> y [_ _ _ defW1y _]. have /idP[]:= negbF cycW; rewrite (cyclic_dprod defW) // /coprime. by rewrite -(cardJg _ y) defW1y cardJg gcdnn -trivg_card1. have [defWx] := conj_of_typeP StypeP x; rewrite -defT. case/(of_typeP_conj TtypeP)=> y [Ty _ defW2y defW1y defWy]. have Wyx: (y * x^-1)%g \in W. by rewrite -defNW !inE /= conjDg conjUg !conjsgM defW2y defW1y defWy !conjsgK. by rewrite -(conjGid (subsetP sWT _ Wyx)) conjsgM (conjGid Ty) defT conjsgK. 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)