proposition: Lemma FTtypeP_pair_cases : {in 'M, forall M, FTtype M == 1%N} \/ exists S, exists T, exists_typeP (fun _ => typeP_pair S T).
proof: Proof. have [_ [| [[S T] [[maxS maxT] [[W1 W2] /=]]]]] := BGsummaryI gT; first by left. set W := W1 <*> W2; set V := W :\: (W1 :|: W2). case=> [[cycW tiV _] [defS defT tiST]] b4 /orP b2 b3. have [cWW /joing_sub[sW1W sW2W]] := (cyclic_abelian cycW, erefl W). have ntV: V != set0 by have [] := andP tiV. suffices{tiST tiV cWW sW1W sW2W b3 b4} tiW12: W1 :&: W2 = 1%g. have defW: W1 \x W2 = W by rewrite dprodEY ?(centSS _ _ cWW). right; exists S, T; exists S _ _ _ defW; split=> // [|M _ /b4[] // x]. by do 2?split; rewrite ?mFT_odd // /normedTI tiV nVW setTI /=. by case=> <-; rewrite inE mem_orbit ?orbT // ?in_setT. wlog {b2 T defT maxT} Stype2: S W1 W2 @W @V maxS defS cycW ntV / FTtype S == 2%N. move=> IH; case/orP: b2 cycW ntV => /IH; first exact. by rewrite setIC /V /W /= joingC setUC; apply. have{maxS Stype2 defS} prW1: prime #|W1|. have [U ? W1x ? ? [[StypeP _ prW1x _] _ _ _ _]] := FTtypeP 2 maxS Stype2. by have /imsetP[x _ ->] := of_typeP_compl_conj StypeP defS; rewrite cardJg. rewrite prime_TIg //; apply: contra ntV => sW12. by rewrite setD_eq0 (setUidPr sW12) join_subG sW12 /=. 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)