proposition: Lemma no_minSimple_odd_group (gT : minSimpleOddGroupType) : False.
proof: Proof. have [/forall_inP | [S [T [_ W W1 W2 defW pairST]]]] := FTtypeP_pair_cases gT. exact/negP/not_all_FTtype1. have xdefW: W2 \x W1 = W by rewrite dprodC. have pairTS := typeP_pair_sym xdefW pairST. pose p := #|W2|; pose q := #|W1|. have p'q: q != p. have [[[ctiW _ _] _ _ _ _] /mulG_sub[sW1W sW2W]] := (pairST, dprodW defW). have [cycW _ _] := ctiW; apply: contraTneq (cycW) => eq_pq. rewrite (cyclic_dprod defW) ?(cyclicS _ cycW) // -/q eq_pq. by rewrite /coprime gcdnn -trivg_card1; have [] := cycTI_nontrivial ctiW. without loss{p'q} ltqp: S T W1 W2 defW xdefW pairST pairTS @p @q / q < p. move=> IH_ST; rewrite neq_ltn in p'q. by case/orP: p'q; [apply: (IH_ST S T) | apply: (IH_ST T S)]. have [[_ maxS maxT] _ _ _ _] := pairST. have [[U StypeP] [V TtypeP]] := (typeP_pairW pairST, typeP_pairW pairTS). have Stype2: FTtype S == 2 := FTtypeP_max_typeII maxS StypeP ltqp. have Ttype2: FTtype T == 2 := FTtypeP_min_typeII maxS maxT StypeP TtypeP ltqp. have /mmax_exists[L maxNU_L]: 'N(U) \proper setT. have [[_ ntU _ _] cUU _ _ _] := compl_of_typeII maxS StypeP Stype2. by rewrite mFT_norm_proper // mFT_sol_proper abelian_sol. have /mmax_exists[M maxNV_M]: 'N(V) \proper setT. have [[_ ntV _ _] cVV _ _ _] := compl_of_typeII maxT TtypeP Ttype2. by rewrite mFT_norm_proper // mFT_sol_proper abelian_sol. have [[maxL sNU_L] [maxM sNV_M]] := (setIdP maxNU_L, setIdP maxNV_M). have [frobL sUH _] := FTtypeII_support_facts maxS StypeP Stype2 pairST maxNU_L. have [frobM _ _] := FTtypeII_support_facts maxT TtypeP Ttype2 pairTS maxNV_M. have Ltype1 := FT_Frobenius_type1 maxL frobL. have Mtype1 := FT_Frobenius_type1 maxM frobM. have [tau1L cohL] := FTtype1_coherence maxL Ltype1. have [tau1M cohM] := FTtype1_coherence maxM Mtype1. have [phi Lphi phi1] := FTtype1_ref_irr maxL. have [psi Mpsi psi1] := FTtype1_ref_irr maxM. exact: (FTtype2_exclusion pairST maxS maxT StypeP TtypeP ltqp maxNU_L sNU_L sUH frobL Ltype1 cohL Lphi phi1 maxNV_M sNV_M frobM Mtype1 cohM Mpsi psi1). Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq path div choice fintype) mathcomp(tuple finfun bigop order prime binomial ssralg poly finset) mathcomp(fingroup morphism perm automorphism quotient action finalg zmodp) mathcomp(gfunctor gproduct center cyclic commutator gseries nilpotent) mathcomp(pgroup sylow hall abelian maximal frobenius) mathcomp(matrix mxalgebra mxrepresentation mxabelem vector) odd_order(BGsection1 BGsection3 BGsection7) odd_order(BGsection14 BGsection15 BGsection16 BGappendixC) mathcomp(ssrnum rat algC cyclotomic algnum) mathcomp(classfun character integral_char inertia vcharacter) odd_order(PFsection1 PFsection2 PFsection3 PFsection4) odd_order(PFsection5 PFsection6 PFsection7 PFsection8 PFsection9) odd_order(PFsection10 PFsection11 PFsection12 PFsection13)