proposition: Lemma FTtype1_nonFrobenius_witness_contradiction : False.
proof: Proof. have pr_p: prime p. by have:= ltnW prankM; rewrite p_rank_gt0 mem_primes => /andP[]. have [sP0M pP0 _] := and3P sylP0; have abelP01 := Ohm1_abelem pP0 abP0. have [ntx P01x] := setD1P P0_1s_x. have ox: #[x] = p := abelem_order_p abelP01 P01x ntx. have odd_p: odd p by rewrite -ox mFT_odd. have pgt2 := odd_prime_gt2 odd_p pr_p. have Zpsi: psi \in 'Z[irr G] by have [[_ ->//]] := cohS; apply: mem_zchar. have lb_psiM: '[rhoM psi] >= #|K :\: K'|%:R / #|M|%:R * e.-1%:R ^+ 2. have [g /setIP[Kg cxg] notK'g] := subsetPn not_sCxK'. have KK'g: g \in K :\: K' by rewrite !inE notK'g. have [rhoMid /(_ _ g _ KK'g)psiKK'_id /(_ g KK'g)Zpsig] := rhoM_psi. rewrite -mulrA mulrCA ler_pM2l ?invr_gt0 ?gt0CG // mulr_natl. rewrite (big_setID (K :\: K')) (setIidPr _) ?subDset ?subsetU ?gFsub ?orbT //. rewrite ler_wpDr ?sumr_ge0 // => [z _|]; first exact: mul_conjC_ge0. rewrite -sumr_const ler_sum // => z KK'z. rewrite {}rhoMid ?(subsetP _ z KK'z) ?setDS ?sub1G // {}psiKK'_id {z KK'z}//. rewrite -normCK ler_sqr ?qualifE/= ?ler0n ?normr_ge0 //. have [eps prim_eps] := C_prim_root_exists (prime_gt0 pr_p). have psi_xg: (psi (x * g)%g == e%:R %[mod 1 - eps])%A. have [-> // _] := rhoL_psi; rewrite -[x]mulg1 -chi1. rewrite (vchar_ker_mod_prim prim_eps) ?group1 ?(seqInd_vcharW Schi) //. by rewrite (subsetP _ _ P01x) // gFsub_trans ?(subset_trans sP0H) ?gFsub. have{psi_xg} /dvdCP[a Za /(canRL (subrK _))->]: (p %| psi g - e%:R)%C. rewrite (int_eqAmod_prime_prim prim_eps) ?rpredB ?rpred_nat // eqAmod0. apply: eqAmod_trans psi_xg; rewrite eqAmod_sym. by rewrite (vchar_ker_mod_prim prim_eps) ?in_setT. have [-> | nz_a] := eqVneq a 0. by rewrite mul0r add0r normr_nat leC_nat leq_pred. rewrite -[e%:R]opprK (le_trans _ (lerB_dist _ _)) // normrN normrM. rewrite lerBrDl !normr_nat -natrD. apply: le_trans (_ : 1 * p%:R <= _); last first. by rewrite ler_wpM2r ?ler0n ?norm_Cint_ge1. rewrite mul1r leC_nat -subn1 addnBA ?cardG_gt0 // leq_subLR addnn -ltnS. have [b e_dv_pb]: exists b : bool, e %| (b.*2 + p).-1. by have [_ /orP[]] := Ecyclic_le_p; [exists false | exists true]. apply: (@leq_trans (b.*2 + p)); last first. by rewrite (leq_add2r p _ 2) (leq_double b 1) leq_b1. rewrite dvdn_double_ltn ?oddD ?mFT_odd ?odd_double //. by rewrite addnC -(subnKC pgt2). have irrS: {subset calS <= irr L} by have [] := FT_Frobenius_coherence maxL. have lb_psiL: '[rhoL psi] >= 1 - e%:R / #|H|%:R. have irr_chi := irrS _ Schi. have Sgt1: (1 < size calS)%N by apply: seqInd_nontrivial (mFT_odd L) _ Schi. have De: #|L : H| = e by rewrite -(index_sdprod defL). have [|_] := Dade_Ind1_sub_lin cohS_H Sgt1 irr_chi Schi; rewrite De //=. by rewrite -De odd_Frobenius_index_ler ?mFT_odd // => -[_ _ []//]. have tiA1_LM: [disjoint 'A1~(L) & 'A1~(M)]. apply: FT_Dade1_support_disjoint => //. apply: contraL p'K => /= /imsetP[z _ ->]; rewrite FcoreJ pgroupJ. by rewrite p'groupEpi (piSg sP0H) // -p_rank_gt0 prankP0. have{tiA1_LM} ub_rhoML: '[rhoM psi] + '[rhoL psi] < 1. have [[Itau1 Ztau1] _] := cohS. have n1psi: '[psi] = 1 by rewrite Itau1 ?mem_zchar ?irrWnorm ?irrS. rewrite -n1psi (cfnormE (cfun_onG psi)) (big_setD1 1%g) ?group1 //=. rewrite mulrDr ltr_pwDl 1?mulr_gt0 ?invr_gt0 ?gt0CG ?exprn_gt0 //. have /dirrP[s [i ->]]: psi \in dirr G. by rewrite dirrE Ztau1 ?mem_zchar ?n1psi /=. by rewrite cfunE normrMsign normr_gt0 irr1_neq0. rewrite (big_setID 'A1~(M)) mulrDr lerD //=. rewrite FTsupp1_type1 // -FT_DadeF_supportE. by rewrite (setIidPr _) ?Dade_support_subD1 ?leC_cfnorm_invDade_support. rewrite (big_setID 'A1~(L)) mulrDr ler_wpDr //=. rewrite mulr_ge0 ?invr_ge0 ?ler0n ?sumr_ge0 // => z _. by rewrite exprn_ge0 ?normr_ge0. rewrite (setIidPr _); last first. by rewrite subsetD tiA1_LM -FT_Dade1_supportE Dade_support_subD1. by rewrite FTsupp1_type1 // -FT_DadeF_supportE leC_cfnorm_invDade_support. have ubM: (#|M| <= #|K| * #|H|)%N. by rewrite -(sdprod_card defM) leq_mul // subset_leq_card. have{lb_psiM lb_psiL ub_rhoML ubM} ubK: (#|K / K'|%g < 4)%N. rewrite card_quotient ?gFnorm -?ltC_nat //. rewrite -ltf_pV2 ?qualifE/= ?gt0CiG ?ltr0n // natf_indexg ?gFsub //. rewrite invfM invrK mulrC -(subrK #|K|%:R #|K'|%:R) mulrDl divff ?neq0CG //. rewrite -opprB mulNr addrC ltrBrDl -ltrBrDr. have /Frobenius_context[_ _ ntE _ _] := set_Frobenius_compl defL frobL. have egt2: (2 < e)%N by rewrite odd_geq ?mFT_odd ?cardG_gt1. have e1_gt0: 0 < e.-1%:R :> algC by rewrite ltr0n -(subnKC egt2). apply: lt_le_trans (_ : e%:R / e.-1%:R ^+ 2 <= _). rewrite ltr_pdivlMr ?exprn_gt0 //. rewrite -(@ltr_pM2r _ #|H|%:R^-1) ?invr_gt0 ?gt0CG // mulrAC. rewrite -(ltrD2r 1) -ltrBlDl -addrA. apply: le_lt_trans ub_rhoML; rewrite lerD //. apply: le_trans lb_psiM; rewrite -natrX ler_wpM2r ?ler0n //. rewrite cardsD (setIidPr _) ?gFsub // -natrB ?subset_leq_card ?gFsub //. rewrite -mulrA ler_wpM2l ?ler0n //. rewrite ler_pdivrMr ?gt0CG // ler_pdivlMl ?gt0CG //. by rewrite ler_pdivrMr ?gt0CG // mulrC -natrM leC_nat. rewrite -(ler_pM2l (gt0CG E)) -/e mulrA -expr2 invfM -exprMn. apply: le_trans (_ : (1 + 2%:R^-1) ^+ 2 <= _). rewrite ler_sqr ?rpred_div ?rpredD ?rpred1 ?rpredV ?rpred_nat //. rewrite -{1}(ltn_predK egt2) mulrSr mulrDl divff ?gt_eqF // lerD2l. rewrite ler_pdivrMr // ler_pdivlMl ?ltr0n //. by rewrite mulr1 leC_nat -(subnKC egt2). rewrite -(@ler_pM2r _ (2 ^ 2)%:R) ?ltr0n // {1}natrX -exprMn -mulrA. rewrite mulrDl mulrBl !mul1r !mulVf ?pnatr_eq0 // (mulrSr _ 3) addrK. by rewrite -mulrSr ler_wpM2r ?ler0n ?ler_nat. have [U [MtypeF _]] := FTtypeP 1 maxM Mtype1. have{U MtypeF} [_ _ [U0 [sU0ML expU0 frobU0]]] := compl_of_typeF defM MtypeF. have [/sdprodP[_ _ nKU0 tiKU0] ntK _ _ _] := Frobenius_context frobU0. have nK'U0: U0 \subset 'N(K') by apply: gFnorm_trans. have frobU0K': [Frobenius K <*> U0 / K' = (K / K') ><| (U0 / K')]%g. have solK: solvable K by rewrite ?nilpotent_sol ?Fcore_nil. rewrite Frobenius_proper_quotient ?(sol_der1_proper solK) // /(_ <| _). by rewrite (subset_trans (der_sub 1 _)) ?joing_subl // join_subG gFnorm. have isoU0: U0 \isog U0 / K'. by rewrite quotient_isog //; apply/trivgP; rewrite -tiKU0 setSI ?gFsub. have piU0p: p \in \pi(U0 / K')%g. rewrite /= -(card_isog isoU0) -pi_of_exponent expU0 pi_of_exponent. rewrite mem_primes pr_p cardG_gt0 /= -ox order_dvdG // (subsetP _ _ P01x) //. by rewrite gFsub_trans // subsetI sP0M (subset_trans sP0H) ?gFsub. have /(Cauchy pr_p)[z U0z oz]: p %| #|U0 / K'|%g. by do [rewrite mem_primes => /and3P[]//] in piU0p. have frobKz: [Frobenius (K / K') <*> <[z]> = (K / K') ><| <[z]>]%g. rewrite (Frobenius_subr _ _ frobU0K') ?cycle_subG //. by rewrite cycle_eq1 -order_gt1 oz ltnW. have: p %| #|K / K'|%g.-1 by rewrite -oz (Frobenius_dvd_ker1 frobKz) //. have [_ ntKK' _ _ _] := Frobenius_context frobKz. rewrite -subn1 gtnNdvd ?subn_gt0 ?cardG_gt1 // subn1 prednK ?cardG_gt0 //. by rewrite -ltnS (leq_trans ubK). Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq path div choice) mathcomp(fintype tuple finfun bigop order prime ssralg finset center) mathcomp(fingroup morphism perm automorphism quotient action finalg zmodp) mathcomp(gfunctor gproduct cyclic commutator gseries nilpotent pgroup) mathcomp(sylow hall abelian maximal frobenius) mathcomp(matrix mxalgebra mxpoly mxrepresentation mxabelem vector) mathcomp(falgebra fieldext finfield) odd_order(BGsection1 BGsection2 BGsection3 BGsection4 BGsection7) odd_order(BGsection14 BGsection15 BGsection16) mathcomp(ssrnum ssrint algC cyclotomic algnum) mathcomp(classfun character inertia vcharacter) odd_order(PFsection1 PFsection2 PFsection3 PFsection4 PFsection5) odd_order(PFsection6 PFsection7 PFsection8 PFsection9 PFsection10) odd_order(PFsection11)