proposition: Lemma typeP_pairW S T W W1 W2 (defW : W1 \x W2 = W) : typeP_pair S T defW -> exists U : {group gT}, of_typeP S U defW.
proof: Proof. case=> [[[cycW _ /and3P[_ _ /eqP nVW]] maxS _] [defS _ defST] _ [Stype25 _] _]. set S' := S^`(1)%g in defS; have [nsS'S _ _ _ tiS'W1] := sdprod_context defS. have{Stype25} Stype'1: FTtype S != 1%N by apply: contraTneq Stype25 => ->. have [/mulG_sub[sW1W sW2W] [_ mulW12 cW12 _]] := (dprodW defW, dprodP defW). have [cycW1 cycW2] := (cyclicS sW1W cycW, cyclicS sW2W cycW). have{cycW1 cycW2} coW12: coprime #|W1| #|W2| by rewrite -(cyclic_dprod defW). have{maxS Stype'1} [Ux Wx W1x W2x defWx StypeP] := FTtypeP_witness maxS Stype'1. have /imsetP[y Sy defW1] := of_typeP_compl_conj StypeP defS. suffices defW2: W2 :=: W2x :^ y. have [] := conj_of_typeP StypeP y; rewrite -defWx dprodJ -defW1 -defW2. by rewrite (conjGid Sy) {-1}defW; exists (Ux :^ y)%G. have [[_ hallW1x _ defSx] _ _ [/cyclic_abelian abW2x _ _ _ _] _] := StypeP. have{Sy} nS'y: y \in 'N(S') by rewrite (subsetP (normal_norm nsS'S)). have{nS'y} defW2xy: W2x :^ y = 'C_S'(W1). by rewrite -(typeP_cent_compl StypeP) conjIg -centJ -defW1 (normP nS'y). have{nsS'S} sW2S': W2 \subset S'. have sW2S: W2 \subset S by rewrite (subset_trans sW2W) // -defST subsetIl. have{hallW1x} hallW1: \pi(W1).-Hall(S) W1x by rewrite defW1 /= cardJg Hall_pi. have hallS': \pi(W1)^'.-Hall(S) S' by apply/(sdprod_normal_pHallP _ hallW1). by rewrite coprime_pi' // (sub_normal_Hall hallS') in coW12 *. have sW2xy: W2 \subset W2x :^ y by rewrite defW2xy subsetI sW2S'. have defW2: W2 :=: S' :&: W by rewrite -mulW12 -group_modr ?tiS'W1 ?mul1g. apply/eqP; rewrite eqEsubset sW2xy defW2 subsetI {1}defW2xy subsetIl /=. rewrite -nVW /= setTI cents_norm // (centsS (subsetDl _ _)) // -mulW12. by rewrite centM subsetI {1}defW2xy subsetIr sub_abelian_cent // abelianJ. 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)