Timings for BGappendixC.v

(* (c) Copyright 2006-2015 Microsoft Corporation and Inria.                  *)
(* Distributed under the terms of CeCILL-B.                                  *)
Require Import mathcomp.ssreflect.ssreflect.
From mathcomp
Require Import ssrbool ssrfun eqtype choice ssrnat seq div fintype.
From mathcomp
Require Import tuple finfun bigop ssralg finset prime binomial poly polydiv.
From mathcomp
Require Import fingroup morphism quotient automorphism action finalg zmodp.
From mathcomp
Require Import gfunctor gproduct cyclic commutator pgroup abelian frobenius.
From mathcomp
Require Import BGsection1.
From mathcomp
Require Import matrix mxalgebra mxabelem vector falgebra fieldext galois.
From mathcomp
Require Import finfield ssrnum algC classfun character integral_char inertia.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Import GroupScope GRing.Theory FinRing.Theory Num.Theory.
Local Open Scope ring_scope.

Section AppendixC.

Variables (gT : finGroupType) (p q : nat) (H P P0 U Q : {group gT}).
Let nU := ((p ^ q).-1 %/ p.-1)%N.

(* External statement of the finite field assumption. *)
CoInductive finFieldImage : Prop :=
  FinFieldImage (F : finFieldType) (sigma : {morphism P >-> F}) of
     isom P [set: F] sigma & sigma @*^-1 <[1 : F]> = P0
   & exists2 sigmaU : {morphism U >-> {unit F}},
     'injm sigmaU & {in P & U, morph_act 'J 'U sigma sigmaU}.

(* These correspond to hypothesis (A) of B & G, Appendix C, Theorem C.        *)
Hypotheses (pr_p : prime p) (pr_q : prime q) (coUp1 : coprime nU p.-1).
Hypotheses (defH : P ><| U = H) (fieldH : finFieldImage).
Hypotheses (oP : #|P| = (p ^ q)%N) (oU : #|U| = nU).

(* These correspond to hypothesis (B) of B & G, Appendix C, Theorem C.        *)
Hypotheses (abelQ : q.-abelem Q) (nQP0 : P0 \subset 'N(Q)).
Hypothesis nU_P0Q : exists2 y, y \in Q & P0 :^ y \subset 'N(U).

Section ExpandHypotheses.

(* Negation of the goal of B & G, Appendix C, Theorem C.                      *)
Hypothesis ltqp : (q < p)%N.

(* From the fieldH assumption. *)
Variables (fT : finFieldType) (charFp : p \in [char fT]).
Local Notation F := (PrimeCharType charFp).
Local Notation galF := [splittingFieldType 'F_p of F].
Let Fpq : {vspace F} := fullv.
Let Fp : {vspace F} := 1%VS.

Hypothesis oF : #|F| = (p ^ q)%N.
Let oF_p : #|'F_p| = p. Proof. exact: card_Fp. Qed.
Let oFp : #|Fp| = p. Proof. by rewrite card_vspace1. Qed.
Let oFpq : #|Fpq| = (p ^ q)%N. Proof. by rewrite card_vspacef. Qed.
Let dimFpq : \dim Fpq = q. Proof. by rewrite primeChar_dimf oF pfactorK. Qed.

Variables (sigma : {morphism P >-> F}) (sigmaU : {morphism U >-> {unit F}}).
Hypotheses (inj_sigma : 'injm sigma) (inj_sigmaU : 'injm sigmaU).
Hypothesis im_sigma : sigma @* P = [set: F].
Variable s : gT.
Hypotheses (sP0P : P0 \subset P) (sigma_s : sigma s = 1) (defP0 : <[s]> = P0).

Let psi u : F := val (sigmaU u).
Let inj_psi : {in U &, injective psi}.
Proof. by move=> u v Uu Uv /val_inj/(injmP inj_sigmaU)->. Qed.

Hypothesis sigmaJ : {in P & U, forall x u, sigma (x ^ u) = sigma x * psi u}.

Let Ps : s \in P. Proof. by rewrite -cycle_subG defP0. Qed.
Let P0s : s \in P0. Proof. by rewrite -defP0 cycle_id. Qed.

Let nz_psi u : psi u != 0. Proof. by rewrite -unitfE (valP (sigmaU u)). Qed.

Let sigma1 : sigma 1%g = 0. Proof. exact: morph1. Qed.
Let sigmaM : {in P &, {morph sigma : x1 x2 / (x1 * x2)%g >-> x1 + x2}}.
Proof. exact: morphM. Qed.
Let sigmaV : {in P, {morph sigma : x / x^-1%g >-> - x}}.
Proof. exact: morphV. Qed.
Let sigmaX n : {in P, {morph sigma : x / (x ^+ n)%g >-> x *+ n}}.
Proof. exact: morphX. Qed.

Let psi1 : psi 1%g = 1. Proof. by rewrite /psi morph1. Qed.
Let psiM : {in U &, {morph psi : u1 u2 / (u1 * u2)%g >-> u1 * u2}}.
Proof. by move=> u1 u2 Uu1 Uu2; rewrite /psi morphM. Qed.
Let psiV : {in U, {morph psi : u / u^-1%g >-> u^-1}}.
Proof. by move=> u Uu; rewrite /psi morphV. Qed.
Let psiX n : {in U, {morph psi : u / (u ^+ n)%g >-> u ^+ n}}.
Proof. by move=> u Uu; rewrite /psi morphX // val_unitX. Qed.

Let sigmaE := (sigma1, sigma_s, mulr1, mul1r,
               (sigmaJ, sigmaX, sigmaM, sigmaV), (psi1, psiX, psiM, psiV)).

Let psiE u : u \in U -> psi u = sigma (s ^ u).
Proof. by move=> Uu; rewrite !sigmaE. Qed.

Let nPU : U \subset 'N(P). Proof. by have [] := sdprodP defH. Qed.
Let memJ_P : {in P & U, forall x u, x ^ u \in P}.
Proof. by move=> x u Px Uu; rewrite /= memJ_norm ?(subsetP nPU). Qed.
Let in_PU := (memJ_P, in_group).

Let sigmaP0 : sigma @* P0 =i Fp.
Proof.
rewrite -defP0 morphim_cycle // sigma_s => x.
apply/cycleP/vlineP=> [] [n ->]; first by exists n%:R; rewrite scaler_nat.
by exists (val n); rewrite -{1}[n]natr_Zp -in_algE rmorph_nat zmodXgE.
Qed.

Let nt_s : s != 1%g.
Proof. by rewrite -(morph_injm_eq1 inj_sigma) // sigmaE oner_eq0. Qed.

Let p_gt0 : (0 < p)%N. Proof. exact: prime_gt0. Qed.
Let q_gt0 : (0 < q)%N. Proof. exact: prime_gt0. Qed.
Let p1_gt0 : (0 < p.-1)%N. Proof. by rewrite -subn1 subn_gt0 prime_gt1. Qed.

(* This is B & G, Appendix C, Remark I. *)
Let not_dvd_q_p1 : ~~ (q %| p.-1)%N.
Proof.
rewrite -prime_coprime // -[q]card_ord -sum1_card -coprime_modl -modn_summ.
have:= coUp1; rewrite /nU predn_exp mulKn //= -coprime_modl -modn_summ.
congr (coprime (_ %% _) _); apply: eq_bigr => i _.
by rewrite -{1}[p](subnK p_gt0) subn1 -modnXm modnDl modnXm exp1n.
Qed.

(* This is the first assertion of B & G, Appendix C, Remark V. *)
Let odd_p : odd p.
Proof.
by apply: contraLR ltqp => /prime_oddPn-> //; rewrite -leqNgt prime_gt1.
Qed.

(* This is the second assertion of B & G, Appendix C, Remark V. *)
Let odd_q : odd q.
Proof.
apply: contraR not_dvd_q_p1 => /prime_oddPn-> //.
by rewrite -subn1 dvdn2 odd_sub ?odd_p.
Qed.

Let qgt2 : (2 < q)%N. Proof. by rewrite odd_prime_gt2. Qed.
Let pgt4 : (4 < p)%N. Proof. by rewrite odd_geq ?(leq_ltn_trans qgt2). Qed.
Let qgt1 : (1 < q)%N. Proof. exact: ltnW. Qed.

Local Notation Nm := (galNorm Fp Fpq).
Local Notation uval := (@FinRing.uval _).

Let cycFU (FU : {group {unit F}}) : cyclic FU.
Proof. exact: field_unit_group_cyclic. Qed.
Let cUU : abelian U.
Proof. by rewrite cyclic_abelian // -(injm_cyclic inj_sigmaU) ?cycFU. Qed.

(* This is B & G, Appendix C, Remark VII. *)
Let im_psi (x : F) : (x \in psi @: U) = (Nm x == 1).
Proof.
have /cyclicP[u0 defFU]: cyclic [set: {unit F}] by apply: cycFU.
have o_u0: #[u0] = (p ^ q).-1 by rewrite orderE -defFU card_finField_unit oF.
have ->: psi @: U = uval @: (sigmaU @* U) by rewrite morphimEdom -imset_comp.
have /set1P[->]: (sigmaU @* U)%G \in [set <[u0 ^+ (#[u0] %/ nU)]>%G].
  rewrite -cycle_sub_group ?inE; last first.
    by rewrite o_u0 -(divnK (dvdn_pred_predX p q)) dvdn_mulr.
  by rewrite -defFU subsetT card_injm //= oU.
rewrite divnA ?dvdn_pred_predX // -o_u0 mulKn //.
have [/= alpha alpha_gen Dalpha] := finField_galois_generator (subvf Fp).
have{Dalpha} Dalpha x1: x1 != 0 -> x1 / alpha x1 = x1^-1 ^+ p.-1.
  move=> nz_x1; rewrite -[_ ^+ _](mulVKf nz_x1) -exprS Dalpha ?memvf // exprVn.
  by rewrite dimv1 oF_p prednK ?prime_gt0.
apply/idP/(Hilbert's_theorem_90 alpha_gen (memvf _)) => [|[u [_ nz_u] ->]].
  case/imsetP=> /= _ /cycleP[n ->] ->; rewrite expgAC; set u := (u0 ^+ n)%g.
  have nz_u: (val u)^-1 != 0 by rewrite -unitfE unitrV (valP u).
  by exists (val u)^-1; rewrite ?memvf ?Dalpha //= invrK val_unitX.
have /cycleP[n Du]: (insubd u0 u)^-1%g \in <[u0]> by rewrite -defFU inE.
have{Du} Du: u^-1 = val (u0 ^+ n)%g by rewrite -Du /= insubdK ?unitfE.
by rewrite Dalpha // Du -val_unitX mem_imset // expgAC mem_cycle.
Qed.

(* This is B & G, Appendix C, Remark VIII. *)
Let defFU : sigmaU @* U \x [set u | uval u \in Fp] = [set: {unit F}].
Proof.
have fP v: in_alg F (uval v) \is a GRing.unit by rewrite rmorph_unit ?(valP v).
pose f (v : {unit 'F_p}) := FinRing.unit F (fP v).
have fM: {in setT &, {morph f: v1 v2 / (v1 * v2)%g}}.
  by move=> v1 v2 _ _; apply: val_inj; rewrite /= -in_algE rmorphM.
pose galFpU := Morphism fM @* [set: {unit 'F_p}].
have ->: [set u | uval u \in Fp] = galFpU.
  apply/setP=> u; rewrite inE /galFpU morphimEdom.
  apply/idP/imsetP=> [|[v _ ->]]; last by rewrite /= rpredZ // memv_line.
  case/vlineP=> v Du; have nz_v: v != 0.
    by apply: contraTneq (valP u) => v0; rewrite unitfE /= Du v0 scale0r eqxx.
  exists (insubd (1%g : {unit 'F_p}) v); rewrite ?inE //.
  by apply: val_inj; rewrite /= insubdK ?unitfE.
have oFpU: #|galFpU| = p.-1.
  rewrite card_injm ?card_finField_unit ?oF_p //.
  by apply/injmP=> v1 v2 _ _ []/(fmorph_inj [rmorphism of in_alg F])/val_inj.
have oUU: #|sigmaU @* U| = nU by rewrite card_injm.
rewrite dprodE ?coprime_TIg ?oUU ?oFpU //; last first.
  by rewrite (sub_abelian_cent2 (cyclic_abelian (cycFU [set: _]))) ?subsetT.
apply/eqP; rewrite eqEcard subsetT coprime_cardMg oUU oFpU //=.
by rewrite card_finField_unit oF divnK ?dvdn_pred_predX.
Qed.

(* This is B & G, Appendix C, Remark IX. *)
Let frobH : [Frobenius H = P ><| U].
Proof.
apply/Frobenius_semiregularP=> // [||u /setD1P[ntu Uu]].
- by rewrite -(morphim_injm_eq1 inj_sigma) // im_sigma finRing_nontrivial.
- rewrite -cardG_gt1 oU ltn_divRL ?dvdn_pred_predX // mul1n -!subn1.
  by rewrite ltn_sub2r ?(ltn_exp2l 0) ?(ltn_exp2l 1) ?prime_gt1.
apply/trivgP/subsetP=> x /setIP[Px /cent1P/commgP].
rewrite inE -!(morph_injm_eq1 inj_sigma) ?(sigmaE, in_PU) //.
rewrite -mulrN1 addrC -mulrDr mulf_eq0 subr_eq0 => /orP[] // /idPn[].
by rewrite (inj_eq val_inj (sigmaU u) 1%g) morph_injm_eq1.
Qed.

(* From the abelQ assumption of Peterfalvi, Theorem (14.2) to the assumptions *)
(* of part (B) of the assumptions of Theorem C.                               *)
Let p'q : q != p. Proof. by rewrite ltn_eqF. Qed.
Let cQQ : abelian Q. Proof. exact: abelem_abelian abelQ. Qed.
Let p'Q : p^'.-group Q. Proof. exact: pi_pgroup (abelem_pgroup abelQ) _. Qed.

Let pP : p.-group P. Proof. by rewrite /pgroup oP pnat_exp ?pnat_id. Qed.
Let coQP : coprime #|Q| #|P|. Proof. exact: p'nat_coprime p'Q pP. Qed.
Let sQP0Q : [~: Q, P0] \subset Q. Proof. by rewrite commg_subl. Qed.

(* This is B & G, Appendix C, Remark X. *)
Let defQ : 'C_Q(P0) \x [~: Q, P0] = Q.
Proof. by rewrite dprodC coprime_abelian_cent_dprod // (coprimegS sP0P). Qed.

(* This is B & G, Appendix C, Remark XI. *)
Let nU_P0QP0 : exists2 y, y \in [~: Q, P0] & P0 :^ y \subset 'N(U).
Proof.
have [_ /(mem_dprod defQ)[z [y [/setIP[_ cP0z] QP0y -> _]]]] := nU_P0Q.
by rewrite conjsgM (normsP (cent_sub P0)) //; exists y.
Qed.

Let E := [set x : galF | Nm x == 1 & Nm (2%:R - x) == 1].

Let E_1 : 1 \in E.
Proof. by rewrite !inE -addrA subrr addr0 galNorm1 eqxx. Qed.

(* This is B & G, Appendix C, Lemma C.1. *)
Let Einv_gt1_le_pq : E = [set x^-1 | x in E] -> (1 < #|E|)%N -> (p <= q)%N.
Proof.
rewrite (cardsD1 1) E_1 ltnS card_gt0 => Einv /set0Pn[/= a /setD1P[not_a1 Ea]].
pose tau (x : F) := (2%:R - x)^-1.
have Etau x: x \in E -> tau x \in E.
  rewrite inE => Ex; rewrite Einv (mem_imset (fun y => y^-1)) //.
  by rewrite inE andbC opprD addNKr opprK.
pose Pa := \prod_(beta in 'Gal(Fpq / Fp)) (beta (1 - a) *: 'X + 1).
have galPoly_roots: all (root (Pa - 1)) (enum Fp).
  apply/allP=> x; rewrite mem_enum => /vlineP[b ->].
  rewrite rootE !hornerE horner_prod subr_eq0 /=; apply/eqP.
  pose h k := (1 - a) *+ k + 1; transitivity (Nm (h b)).
    apply: eq_bigr => beta _; rewrite !(rmorphB, rmorphD, rmorphMn) rmorph1 /=.
    by rewrite -mulr_natr -scaler_nat natr_Zp hornerD hornerZ hornerX hornerC.
  elim: (b : nat) => [|k IHk]; first by rewrite /h add0r galNorm1.
  suffices{IHk}: h k / h k.+1 \in E.
    rewrite inE -invr_eq1 => /andP[/eqP <- _].
    by rewrite galNormM galNormV /= [galNorm _ _ (h k)]IHk mul1r invrK.
  elim: k => [|k IHk]; first by rewrite /h add0r mul1r addrAC Etau.
  have nz_hk1: h k.+1 != 0.
    apply: contraTneq IHk => ->; rewrite invr0 mulr0.
    by rewrite inE galNorm0 eq_sym oner_eq0.
  congr (_ \in E): (Etau _ IHk); apply: canLR (@invrK _) _; rewrite invfM invrK.
  apply: canRL (mulKf nz_hk1) _; rewrite mulrC mulrBl divfK // mulrDl mul1r.
  by rewrite {2}/h mulrS -2!addrA addrK addrAC -mulrSr.
have sizePa: size Pa = q.+1.
  have sizePaX (beta : {rmorphism F -> F}) : size (beta (1 - a) *: 'X + 1) = 2.
    rewrite -mul_polyC size_MXaddC oner_eq0 andbF size_polyC fmorph_eq0.
    by rewrite subr_eq0 eq_sym (negbTE not_a1).
  rewrite size_prod => [|i _]; last by rewrite -size_poly_eq0 sizePaX.
  rewrite (eq_bigr (fun _ => 2)) => [|beta _]; last by rewrite sizePaX.
  rewrite sum_nat_const muln2 -addnn -addSn addnK.
  by rewrite -galois_dim ?finField_galois ?subvf // dimv1 divn1 dimFpq.
have sizePa1: size (Pa - 1) = q.+1.
  by rewrite size_addl // size_opp size_poly1 sizePa.
have nz_Pa1 : Pa - 1 != 0 by rewrite -size_poly_eq0 sizePa1.
by rewrite -ltnS -oFp -sizePa1 cardE max_poly_roots ?enum_uniq.
Qed.

(* This is B & G, Appendix C, Lemma C.2. *)
Let E_gt1 : (1 < #|E|)%N.
Proof.
have [q_gt4 | q_le4] := ltnP 4 q.
  pose inK x := enum_rank_in (classes1 H) (x ^: H).
  have inK_E x: x \in H -> enum_val (inK x) = x ^: H.
    by move=> Hx; rewrite enum_rankK_in ?mem_classes. 
  pose j := inK s; pose k := inK (s ^+ 2)%g; pose e := gring_classM_coef j j k.
  have cPP: abelian P by rewrite -(injm_abelian inj_sigma) ?zmod_abelian.
  have Hs: s \in H by rewrite -(sdprodW defH) -[s]mulg1 mem_mulg.
  have DsH n: (s ^+ n) ^: H = (s ^+ n) ^: U.
    rewrite -(sdprodW defH) classM (abelian_classP _ cPP) ?groupX //.
    by rewrite class_support_set1l.
  have injJU: {in U &, injective (conjg s)}.
    by move=> u v Uu Uv eq_s_uv; apply/inj_psi; rewrite ?psiE ?eq_s_uv.
  have ->: #|E| = e.
    rewrite /e /gring_classM_coef !inK_E ?groupX //.
    transitivity #|[set u in U | s^-1 ^ u * s ^+ 2 \in s ^: U]%g|.
      rewrite -(card_in_imset (sub_in2 _ inj_psi)) => [|u /setIdP[] //].
      apply: eq_card => x; rewrite inE -!im_psi.
      apply/andP/imsetP=> [[/imsetP[u Uu ->] /imsetP[v Uv Dv]]{x} | ].
        exists u; rewrite // inE Uu /=; apply/imsetP; exists v => //.
        by apply: (injmP inj_sigma); rewrite ?(sigmaE, in_PU) // mulN1r addrC.
      case=> u /setIdP[Uu /imsetP[v Uv /(congr1 sigma)]].
      rewrite ?(sigmaE, in_PU) // mulN1r addrC => Dv ->.
      by rewrite Dv !mem_imset.
    rewrite DsH (DsH 1%N) expg1; have [w Uw ->] := repr_class U (s ^+ 2).
    pose f u := (s ^ (u * w), (s^-1 ^ u * s ^+ 2) ^ w).
    rewrite -(@card_in_imset _ _ f) => [|u v]; last first.
      by move=> /setIdP[Uu _] /setIdP[Uv _] [/injJU/mulIg-> //]; apply: groupM.
    apply: eq_card => [[x1 x2]]; rewrite inE -andbA.
    apply/imsetP/and3P=> [[u /setIdP[Uu sUs2u'] [-> ->]{x1 x2}] | []].
      rewrite /= conjgM -(rcoset_id Uw) class_rcoset !memJ_conjg mem_orbit //.
      by rewrite sUs2u' -conjMg conjVg mulKVg.
    case/imsetP=> u Uu /= -> sUx2 /eqP/(canRL (mulKg _)) Dx2.
    exists (u * w^-1)%g; last first.
      by rewrite /f /= conjMg -conjgM mulgKV conjVg -Dx2.
    rewrite inE !in_PU // Uw -(memJ_conjg _ w) -class_rcoset rcoset_id //.
    by rewrite conjMg -conjgM mulgKV conjVg -Dx2.
  pose chi_s2 i := 'chi[H]_i s ^+ 2 * ('chi_i (s ^+ 2)%g)^* / 'chi_i 1%g.
  have De: e%:R = #|U|%:R / #|P|%:R * (\sum_i chi_s2 i).
    have Ks: s \in enum_val j by rewrite inK_E ?class_refl.
    have Ks2: (s ^+ 2)%g \in enum_val k by rewrite inK_E ?groupX ?class_refl.
    rewrite (gring_classM_coef_sum_eq Ks Ks Ks2) inK_E //; congr (_ * _).
    have ->: #|s ^: H| = #|U| by rewrite (DsH 1%N) (card_in_imset injJU).
    by rewrite -(sdprod_card defH) mulnC !natrM invfM mulrA mulfK ?neq0CG.
  pose linH := [pred i | P \subset cfker 'chi[H]_i].
  have nsPH: P <| H by have [] := sdprod_context defH.
  have sum_linH: \sum_(i in linH) chi_s2 i = #|U|%:R.
    have isoU: U \isog H / P := sdprod_isog defH.
    have abHbar: abelian (H / P) by rewrite -(isog_abelian isoU).
    rewrite (card_isog isoU) -(card_Iirr_abelian abHbar) -sumr_const.
    rewrite (reindex _ (mod_Iirr_bij nsPH)) /chi_s2 /=.
    apply: eq_big => [i | i _]; rewrite ?mod_IirrE ?cfker_mod //.
    have lin_i: ('chi_i %% P)%CF \is a linear_char.
      exact/cfMod_lin_char/char_abelianP.
    rewrite lin_char1 // divr1 -lin_charX // -normCK.
    by rewrite normC_lin_char ?groupX ?expr1n.
  have degU i: i \notin linH -> 'chi_i 1%g = #|U|%:R.
    case/(Frobenius_Ind_irrP (FrobeniusWker frobH)) => {i}i _ ->.
    rewrite cfInd1 ?normal_sub // -(index_sdprod defH) lin_char1 ?mulr1 //.
    exact/char_abelianP.
  have ub_linH' m (s_m := (s ^+ m)%g):
    (0 < m < 5)%N -> \sum_(i in predC linH) `|'chi_i s_m| ^+ 2 <= #|P|%:R.
  - case/andP=> m_gt0 m_lt5; have{m_gt0 m_lt5} P1sm: s_m \in P^#.
      rewrite !inE groupX // -order_dvdn -(order_injm inj_sigma) // sigmaE.
      by rewrite andbT order_primeChar ?oner_neq0 ?gtnNdvd ?(leq_trans m_lt5).
    have ->: #|P| = (#|P| * (s_m \in s_m ^: H))%N by rewrite class_refl ?muln1.
    have{P1sm} /eqP <-: 'C_H[s ^+ m] == P.
      rewrite eqEsubset (Frobenius_cent1_ker frobH) // subsetI normal_sub //=.
      by rewrite sub_cent1 groupX // (subsetP cPP).
    rewrite mulrnA -second_orthogonality_relation ?groupX // big_mkcond.
    by apply: ler_sum => i _; rewrite normCK; case: ifP; rewrite ?mul_conjC_ge0.
  have sqrtP_gt0: 0 < sqrtC #|P|%:R by rewrite sqrtC_gt0 ?gt0CG.
  have{De ub_linH'}: `|(#|P| * e)%:R - #|U|%:R ^+ 2| <= #|P|%:R * sqrtC #|P|%:R.
    rewrite natrM De mulrCA mulrA divfK ?neq0CG // (bigID linH) /= sum_linH.
    rewrite mulrDr addrC addKr mulrC mulr_suml /chi_s2.
    rewrite (ler_trans (ler_norm_sum _ _ _)) // -ler_pdivr_mulr // mulr_suml.
    apply: ler_trans (ub_linH' 1%N isT); apply: ler_sum => i linH'i.
    rewrite ler_pdivr_mulr // degU ?divfK ?neq0CG //.
    rewrite normrM -normrX norm_conjC ler_wpmul2l ?normr_ge0 //.
    rewrite -ler_sqr ?qualifE ?normr_ge0 ?(@ltrW _ 0) // sqrtCK. 
    apply: ler_trans (ub_linH' 2 isT); rewrite (bigD1 i) ?ler_paddr //=.
    by apply: sumr_ge0 => i1 _; rewrite exprn_ge0 ?normr_ge0.
  rewrite natrM real_ler_distl ?rpredB ?rpredM ?rpred_nat // => /andP[lb_Pe _]. 
  rewrite -ltC_nat -(ltr_pmul2l (gt0CG P)) {lb_Pe}(ltr_le_trans _ lb_Pe) //.
  rewrite ltr_subr_addl (@ler_lt_trans _ ((p ^ q.-1)%:R ^+ 2)) //; last first.
    rewrite  -!natrX ltC_nat ltn_sqr oU ltn_divRL ?dvdn_pred_predX //.
    rewrite -(subnKC qgt1) /= -!subn1 mulnBr muln1 -expnSr.
    by rewrite ltn_sub2l ?(ltn_exp2l 0) // prime_gt1.
  rewrite -mulrDr -natrX -expnM muln2 -subn1 doubleB -addnn -addnBA // subn2.
  rewrite expnD natrM -oP ler_wpmul2l ?ler0n //.
  apply: ler_trans (_ : 2%:R * sqrtC #|P|%:R <= _).
    rewrite mulrDl mul1r ler_add2l -(@expr_ge1 _ 2) ?(ltrW sqrtP_gt0) // sqrtCK.
    by rewrite oP natrX expr_ge1 ?ler0n ?ler1n.
  rewrite -ler_sqr ?rpredM ?rpred_nat ?qualifE ?(ltrW sqrtP_gt0) //.
  rewrite exprMn sqrtCK -!natrX -natrM leC_nat -expnM muln2 oP.
  rewrite -(subnKC q_gt4) doubleS (expnS p _.*2.+1) -(subnKC pgt4) leq_mul //.
  by rewrite ?leq_exp2l // !doubleS !ltnS -addnn leq_addl.
have q3: q = 3 by apply/eqP; rewrite eqn_leq qgt2 andbT -ltnS -(odd_ltn 5).
rewrite (cardsD1 1) E_1 ltnS card_gt0; apply/set0Pn => /=.
pose f (c : 'F_p) : {poly 'F_p} := 'X * ('X - 2%:R%:P) * ('X - c%:P) + ('X - 1).
have fc0 c: (f c).[0] = -1 by rewrite !hornerE.
have fc2 c: (f c).[2%:R] = 1 by rewrite !(subrr, hornerE) /= addrK.
have /existsP[c nz_fc]: [exists c, ~~ [exists d, root (f c) d]].
  have nz_f_0 c: ~~ root (f c) 0 by rewrite /root fc0 oppr_eq0.
  rewrite -negb_forall; apply/negP=> /'forall_existsP/fin_all_exists[/= rf rfP].
  suffices inj_rf: injective rf.
    by have /negP[] := nz_f_0 (invF inj_rf 0); rewrite -{2}[0](f_invF inj_rf).
  move=> a b eq_rf_ab; apply/oppr_inj/(addrI (rf a)).
  have: (f a).[rf a] = (f b).[rf a] by rewrite {2}eq_rf_ab !(rootP _).
  rewrite !(hornerXsubC, hornerD, hornerM) hornerX => /addIr/mulfI-> //.
  rewrite mulf_neq0 ?subr_eq0 1?(contraTneq _ (rfP a)) // => -> //.
  by rewrite /root fc2.
have{nz_fc} /= nz_fc: ~~ root (f c) _ by apply/forallP; rewrite -negb_exists.
have sz_fc_lhs: size ('X * ('X - 2%:R%:P) * ('X - c%:P)) = 4.
  by rewrite !(size_mul, =^~ size_poly_eq0) ?size_polyX ?size_XsubC.
have sz_fc: size (f c) = 4 by rewrite size_addl ?size_XsubC sz_fc_lhs.
have irr_fc: irreducible_poly (f c) by apply: cubic_irreducible; rewrite ?sz_fc.
have fc_monic : f c \is monic.
  rewrite monicE lead_coefDl ?size_XsubC ?sz_fc_lhs // -monicE.
  by rewrite !monicMl ?monicXsubC ?monicX.
pose inF := [rmorphism of in_alg F]; pose fcF := map_poly inF (f c).
have /existsP[a fcFa_0]: [exists a : F, root fcF a].
  suffices: ~~ coprimep (f c) ('X ^+ #|F| - 'X).
    apply: contraR; rewrite -(coprimep_map inF) negb_exists => /forallP-nz_fcF.
    rewrite -/fcF rmorphB rmorphX /= map_polyX finField_genPoly.
    elim/big_rec: _ => [|x gF _ co_fcFg]; first exact: coprimep1.
    by rewrite coprimep_mulr coprimep_XsubC nz_fcF.
  have /irredp_FAdjoin[L dimL [z /coprimep_root fcz0 _]] := irr_fc.
  pose finL := [vectType 'F_p of FinFieldExtType L].
  set fcL := map_poly _ _ in fcz0; pose inL := [rmorphism of in_alg L].
  rewrite -(coprimep_map inL) -/fcL rmorphB rmorphX /= map_polyX.
  apply: contraL (fcz0 _) _; rewrite hornerD hornerN hornerXn hornerX subr_eq0.
  have ->: #|F| = #|{: finL}%VS| by rewrite oF card_vspace dimL sz_fc oF_p q3.
  by rewrite card_vspacef (expf_card (z : finL)).
have Fp_fcF: fcF \is a polyOver Fp.
  by apply/polyOverP => i; rewrite coef_map /= memvZ ?memv_line.
pose G := 'Gal(Fpq / Fp).
have galG: galois Fp Fpq by rewrite finField_galois ?subvf.
have oG: #|G| = 3 by rewrite -galois_dim // dimv1 dimFpq q3.
have Fp'a: a \notin Fp.
  by apply: contraL fcFa_0 => /vlineP[d ->]; rewrite fmorph_root.
have DfcF: fcF = \prod_(beta in G) ('X - (beta a)%:P).
  pose Pa : {poly F} := minPoly Fp a.
  have /eqP szPa: size Pa == 4.
    rewrite size_minPoly eqSS.
    rewrite (sameP eqP (prime_nt_dvdP _ _)) ?adjoin_deg_eq1 //.
    by rewrite adjoin_degreeE dimv1 divn1 -q3 -dimFpq field_dimS ?subvf.
  have dvd_Pa_fcF: Pa %| fcF by apply: minPoly_dvdp fcFa_0.
  have{dvd_Pa_fcF} /eqP <-: Pa == fcF.
    rewrite -eqp_monic ?monic_minPoly ?monic_map // -dvdp_size_eqp //.
    by rewrite szPa size_map_poly sz_fc.
  have [r [srG /map_uniq Ur defPa]]:= galois_factors (subvf _) galG a (memvf a).
  rewrite -/Pa big_map in defPa; rewrite defPa big_uniq //=.
  apply/eq_bigl/subset_cardP=> //; apply/eqP.
  by rewrite -eqSS (card_uniqP Ur) oG -szPa defPa size_prod_XsubC.
exists a; rewrite !inE; apply/and3P; split.
- by apply: contraNneq Fp'a => ->; apply: mem1v.
- apply/eqP; transitivity ((- 1) ^+ #|G| * fcF.[inF 0]).
    rewrite DfcF horner_prod -prodrN; apply: eq_bigr => beta _.
    by rewrite rmorph0 hornerXsubC add0r opprK.
  by rewrite -signr_odd mulr_sign oG horner_map fc0 rmorphN1 opprK.
apply/eqP; transitivity (fcF.[inF 2%:R]); last by rewrite horner_map fc2 rmorph1.
rewrite DfcF horner_prod; apply: eq_bigr => beta _.
by rewrite hornerXsubC rmorphB !rmorph_nat.
Qed.

Section AppendixC3.

Import GroupScope.

Variables y : gT.
Hypotheses (QP0y : y \in [~: Q, P0]) (nUP0y : P0 :^ y \subset 'N(U)).
Let Qy : y \in Q. Proof. by rewrite (subsetP sQP0Q). Qed.

Let t := s ^ y.
Let P1 := P0 :^ y.

(* This is B & G, Appendix C, Lemma C.3, Step 1. *)
Let splitH x :
     x \in H ->
  exists2 u, u \in U & exists2 v, v \in U & exists2 s1, s1 \in P0
  & x = u * s1 * v.
Proof.
case/(mem_sdprod defH) => z [v [Pz Uv -> _]].
have [-> | nt_z] := eqVneq z 1.
  by exists 1 => //; exists v => //; exists 1; rewrite ?mulg1.
have nz_z: sigma z != 0 by rewrite (morph_injm_eq1 inj_sigma).
have /(mem_dprod defFU)[]: finField_unit nz_z \in setT := in_setT _.
move=> _ [w [/morphimP[u Uu _ ->] Fp_w /(congr1 val)/= Dz _]].
have{Fp_w Dz} [n Dz]: exists n, sigma z = sigma ((s ^+ n) ^ u).
  move: Fp_w; rewrite {}Dz inE => /vlineP[n ->]; exists n.
  by rewrite -{1}(natr_Zp n) scaler_nat mulr_natr conjXg !sigmaE ?in_PU.
exists u^-1; last exists (u * v); rewrite ?groupV ?groupM //.
exists (s ^+ n); rewrite ?groupX // mulgA; congr (_ * _).
by apply: (injmP inj_sigma); rewrite -?mulgA ?in_PU.
Qed.

(* This is B & G, Appendix C, Lemma C.3, Step 2. *)
Let not_splitU s1 s2 u :
  s1 \in P0 -> s2 \in P0 -> u \in U -> s1 * u * s2 \in U ->
  (s1 == 1) && (s2 == 1) || (u == 1) && (s1 * s2 == 1).
Proof.
move=> P0s1 P0s2 Uu; have [_ _ _ tiPU] := sdprodP defH.
have [Ps1 Ps2]: s1 \in P /\ s2 \in P by rewrite !(subsetP sP0P).
have [-> | nt_s1 /=] := altP (s1 =P 1).
  by rewrite mul1g groupMl // -in_set1 -set1gE -tiPU inE Ps2 => ->.
have [-> | nt_u /=] := altP (u =P 1).
  by rewrite mulg1 -in_set1 -set1gE -tiPU inE (groupM Ps1).
rewrite (conjgC _ u) -mulgA groupMl // => Us12; case/negP: nt_u.
rewrite -(morph_injm_eq1 inj_sigmaU) // -in_set1 -set1gE.
have [_ _ _ <-] := dprodP defFU; rewrite !inE mem_morphim //= -/(psi u).
have{Us12}: s1 ^ u * s2 == 1.
  by rewrite -in_set1 -set1gE -tiPU inE Us12 andbT !in_PU.
rewrite -(morph_injm_eq1 inj_sigma) ?(in_PU, sigmaE) // addr_eq0.
move/eqP/(canRL (mulKf _))->; rewrite ?morph_injm_eq1 //.
by rewrite mulrC rpred_div ?rpredN //= -sigmaP0 mem_morphim.
Qed.

(* This is B & G, Appendix C, Lemma C.3, Step 3. *)
Let tiH_P1 t1 : t1 \in P1^# -> H :&: H :^ t1 = U.
Proof.
case/setD1P=>[nt_t1 P1t1]; set X := H :&: _.
have [nsPH sUH _ _ tiPU] := sdprod_context defH.
have sUX: U \subset X.
  by rewrite subsetI sUH -(normsP nUP0y t1 P1t1) conjSg.
have defX: (P :&: X) * U = X.
  by rewrite setIC group_modr // (sdprodW defH) setIAC setIid.
have [tiPX | ntPX] := eqVneq (P :&: X) 1; first by rewrite -defX tiPX mul1g.
have irrPU: acts_irreducibly U P 'J.
  apply/mingroupP; (split=> [|V /andP[ntV]]; rewrite astabsJ) => [|nVU sVP].
    by have [_ ->] := Frobenius_context frobH.
  apply/eqP; rewrite eqEsubset sVP; apply/subsetP=> x Px.
  have [-> // | ntx] := eqVneq x 1.
  have [z Vz ntz] := trivgPn _ ntV; have Pz := subsetP sVP z Vz.
  have nz_z: sigma z != 0%R by rewrite morph_injm_eq1.
  have uP: (sigma x / sigma z)%R \is a GRing.unit.
    by rewrite unitfE mulf_neq0 ?invr_eq0 ?morph_injm_eq1.
  have: FinRing.unit F uP \in setT := in_setT _.
  case/(mem_dprod defFU)=> _ [s1 [/morphimP[u Uu _ ->]]].
  rewrite inE => /vlineP[n Ds1] /(congr1 val)/= Dx _.
  suffices ->: x = (z ^ u) ^+ n by rewrite groupX ?memJ_norm ?(subsetP nVU).
  apply: (injmP inj_sigma); rewrite ?(in_PU, sigmaE) //.
  by rewrite -mulr_natr -scaler_nat natr_Zp -Ds1 -mulrA -Dx mulrC divfK.
have{ntPX defX irrPU} defX: X :=: H.
  rewrite -(sdprodW defH) -defX; congr (_ * _).
  have [_ -> //] := mingroupP irrPU; rewrite ?subsetIl //= -/X astabsJ ntPX.
  by rewrite normsI // normsG.
have nHt1: t1 \in 'N(H) by rewrite -groupV inE sub_conjgV; apply/setIidPl.
have oP0: #|P0| = p by rewrite -(card_injm inj_sigma) // (eq_card sigmaP0) oFp.
have{nHt1} nHP1: P1 \subset 'N(H).
  apply: prime_meetG; first by rewrite cardJg oP0.
  by apply/trivgPn; exists t1; rewrite // inE P1t1.
have{nHP1} nPP1: P1 \subset 'N(P).
  have /Hall_pi hallP: Hall H P by apply: Frobenius_ker_Hall frobH.
  by rewrite -(normal_Hall_pcore hallP nsPH) gFnorm_trans.
have sylP0: p.-Sylow(Q <*> P0) P0.
  rewrite /pHall -divgS joing_subr ?(pgroupS sP0P) //=.
  by rewrite norm_joinEr // coprime_cardMg ?(coprimegS sP0P) ?mulnK.
have sP1QP0: P1 \subset Q <*> P0.
  by rewrite conj_subG ?joing_subr ?mem_gen // inE Qy.
have nP10: P1 \subset 'N(P0).
  have: P1 \subset 'N(P :&: (Q <*> P0)) by rewrite normsI // normsG.
  by rewrite norm_joinEr // -group_modr // setIC coprime_TIg // mul1g.
have eqP10: P1 :=: P0.
  apply/eqP; rewrite eqEcard cardJg leqnn andbT.
  rewrite (comm_sub_max_pgroup (Hall_max sylP0)) //; last exact: normC.
  by rewrite pgroupJ (pHall_pgroup sylP0).
have /idPn[] := prime_gt1 pr_p.
rewrite -oP0 cardG_gt1 negbK -subG1 -(Frobenius_trivg_cent frobH) subsetI sP0P.
apply/commG1P/trivgP; rewrite -tiPU commg_subI // subsetI ?subxx //.
by rewrite sP0P -eqP10.
Qed.

(* This is B & G, Appendix C, Lemma C.3, Step 4. *)
Fact BGappendixC3_Ediv : E = [set x^-1 | x in E]%R.
Proof.
suffices sEV_E: [set x^-1 | x in E]%R \subset E.
  by apply/esym/eqP; rewrite eqEcard sEV_E card_imset //=; apply: invr_inj.
have /mulG_sub[/(subset_trans sP0P)/subsetP-sP0H /subsetP-sUH] := sdprodW defH.
have Hs := sP0H s P0s; have P1t: t \in P1 by rewrite memJ_conjg.
have nUP1 t1: t1 \in P1 -> U :^ t1 = U by move/(subsetP nUP0y)/normP.
have nUtn n u: u \in U -> u ^ (t ^+ n) \in U.
  by rewrite -mem_conjgV nUP1 ?groupV ?groupX.
have nUtVn n u: u \in U -> u ^ (t ^- n) \in U.
  by rewrite -mem_conjg nUP1 ?groupX.
have Qsti i: s ^- i * t ^+ i \in Q.
  by rewrite -conjXg -commgEl (subsetP sQP0Q) // commGC mem_commg ?groupX.
pose is_sUs m a j n u s1 v :=
  [/\ a \in U, u \in U, v \in U, s1 \in P0
    & s ^+ m * a ^ t ^+ j * s ^- n = u * s1 * v].
have split_sUs m a j n:
  a \in U -> exists u, exists s1, exists v, is_sUs m a j n u s1 v.
- move=> Ua; suffices: s ^+ m * a ^ t ^+ j * s ^- n \in H.
    by case/splitH=> u Uu [v Uv [s1 P0s1 Dusv1]]; exists u, s1, v.
  by rewrite 2?groupM ?groupV ?groupX // sUH ?nUtn.
have nt_sUs m j n a u s1 v:
  (m == n.+1) || (n == m.+1) -> is_sUs m a j n u s1 v -> s1 != 1.
- move/pred2P=> Dmn [Ua Uu Uv _ Dusv]; have{Dmn}: s ^+ m != s ^+ n.
    by case: Dmn => ->; last rewrite eq_sym; rewrite expgS eq_mulgV1 ?mulgK.
  apply: contraNneq => s1_1; rewrite {s1}s1_1 mulg1 in Dusv.
  have:= groupM Uu Uv; rewrite -Dusv => /(not_splitU _ _ (nUtn j a Ua))/orP.
  by rewrite !in_group // eq_invg1 -eq_mulgV1 => -[]// /andP[? /eqP->].
have sUs_modP m a j n u s1 v: is_sUs m a j n u s1 v -> a ^ t ^+ j = u * v.
  have [nUP /isom_inj/injmP/=quoUP_inj] := sdprod_isom defH.
  case=> Ua Uu Uv P0s1 /(congr1 (coset P)); rewrite (conjgCV u) -(mulgA _ u).
  rewrite coset_kerr ?groupV 2?coset_kerl ?groupX //; last first.
    by rewrite -mem_conjg (normsP nUP) // (subsetP sP0P).
  by move/quoUP_inj->; rewrite ?nUtn ?groupM.
have expUMp u v Uu Uv := expgMn p (centsP cUU u v Uu Uv).
have sUsXp m a j n u s1 v:
  is_sUs m a j n u s1 v -> is_sUs m (a ^+ p) j n (u ^+ p) s1 (v ^+ p).
- move=> Dusv; have{Dusv} [/sUs_modP Duv [Ua Uu Vv P0s1 Dusv]] := (Dusv, Dusv).
  split; rewrite ?groupX //; move: P0s1 Dusv; rewrite -defP0 => /cycleP[k ->].
  rewrite conjXg -!(mulgA _ (s ^+ k)) ![s ^+ k * _]conjgC 2!mulgA -expUMp //.
  rewrite {}Duv ![s ^+ m * _]conjgC !conjXg -![_ * _ * s ^- n]mulgA.
  move/mulgI/(congr1 (Frobenius_aut charFp \o sigma))=> /= Duv_p.
  congr (_ * _); apply/(injmP inj_sigma); rewrite ?in_PU //.
  by rewrite !{1}sigmaE ?in_PU // rmorphB !rmorphMn rmorph1 in Duv_p *.
have odd_P: odd #|P| by rewrite oP odd_exp odd_p orbT.
suffices EpsiV a: a \in U -> psi a \in E -> psi (a^-1 ^ t ^+ 3) \in E.
  apply/subsetP => _ /imsetP[x Ex ->].
  have /imsetP[a Ua Dx]: x \in psi @: U by rewrite im_psi; case/setIdP: Ex.
  suffices: psi (a^-1 ^ t ^+ (3 * #|P|)) \in E.
    rewrite Dx -psiV // -{2}(conjg1 a^-1); congr (psi (_ ^ _) \in E).
    by apply/eqP; rewrite -order_dvdn orderJ dvdn_mull ?order_dvdG.
  rewrite -(odd_double_half #|P|) odd_P addnC.
  elim: _./2 => [|n /EpsiV/EpsiV/=]; first by rewrite EpsiV -?Dx.
  by rewrite conjVg invgK -!conjgM -!expgD -!mulnSr !(groupV, nUtn) //; apply.
move=> Ua Ea; have{Ea} [b Ub Dab]: exists2 b, b \in U & psi a + psi b = 2%:R.
  case/setIdP: Ea => _; rewrite -im_psi => /imsetP[b Ub Db]; exists b => //.
  by rewrite -Db addrC subrK.
(* In the book k is arbitrary in Fp; however only k := 3 is used. *)
have [u2 [s2 [v2 usv2P]]] := split_sUs 3 (a * _) 2 1%N (groupM Ua (groupVr Ub)).
have{Ua} [u1 [s1 [v1 usv1P]]] := split_sUs 1%N a^-1 3 2 (groupVr Ua).
have{Ub} [u3 [s3 [v3 usv3P]]] := split_sUs 2 b 1%N 3 Ub.
pose s2def w1 w2 w3 := t * s2^-1 * t = w1 * s3 * w2 * t ^+ 2 * s1 * w3.
pose w1 := v2 ^ t^-1 * u3; pose w2 := v3 * u1 ^ t ^- 2; pose w3 := v1 * u2 ^ t.
have stXC m n: (m <= n)%N -> s ^- n ^ t ^+ m = s ^- m ^ t ^+ n * s ^- (n - m).
  move/subnK=> Dn; apply/(mulgI (s ^- (n - m) * t ^+ n))/(mulIg (t ^+ (n - m))).
  rewrite -{1}[in t ^+ n]Dn expgD !mulgA !mulgK -invMg -2!mulgA -!expgD.
  by rewrite addnC Dn (centsP (abelem_abelian abelQ)) ?mulgA.
wlog suffices Ds2: a b u1 v1 u2 v2 u3 v3 @w1 @w2 @w3 Dab usv1P usv2P usv3P /
  s2def w1 w2 w3; last first.
- apply/esym; rewrite -[_ * t]mulgA [_ * t]conjgC mulgA -(expgS _ 1) conjVg.
  rewrite /w2 mulgA; apply: (canRL (mulKVg _)); rewrite 2!mulgA -conjgE.
  rewrite conjMg conjgKV /w3 mulgA; apply: (canLR (mulgKV _)).
  rewrite /w1 -4!mulgA (mulgA u1) (mulgA u3) conjMg -conjgM mulKg -mulgA.
  have [[[Ua _ _ _ <-] [_ _ _ _ Ds2]] [Ub _ _ _ <-]] := (usv1P, usv2P, usv3P).
  apply: (canLR (mulKVg _)); rewrite -!invMg -!conjMg -{}Ds2 groupV in Ua *.
  rewrite -[t]expg1 2!conjMg -conjgM -expgS 2!conjMg -conjgM -expgSr mulgA.
  apply: (canLR (mulgK _)); rewrite 2!invMg -!conjVg invgK invMg invgK -4!mulgA.
  rewrite (mulgA _ s) stXC // mulgKV -!conjMg stXC // mulgKV -conjMg conjgM.
  apply: (canLR (mulKVg _)); rewrite -2!conjVg 2!mulgA -conjMg (stXC 1%N) //.
  rewrite mulgKV -conjgM -expgSr -mulgA -!conjMg; congr (_ ^ t ^+ 3).
  apply/(canLR (mulKVg _))/(canLR (mulgK _))/(canLR invgK).
  rewrite -!mulgA (mulgA _ b) mulgA invMg -!conjVg !invgK.
  by apply/(injmP inj_sigma); rewrite 1?groupM ?sigmaE ?memJ_P.
have [[Ua Uu1 Uv1 P0s1 Dusv1] /sUs_modP-Duv1] := (usv1P, usv1P).
have [[_ Uu2 Uv2 P0s2 _] [Ub Uu3 Uv3 P0s3 _]] := (usv2P, usv3P).
suffices /(congr1 sigma): s ^+ 2 = s ^ v1 * s ^ a^-1 ^ t ^+ 3.
  rewrite inE sigmaX // sigma_s sigmaM ?memJ_P -?psiE ?nUtn // => ->.
  by rewrite addrK -!im_psi !mem_imset ?nUtn.
rewrite groupV in Ua; have [Hs1 Hs3]: s1 \in H /\ s3 \in H by rewrite !sP0H.
have nt_s1: s1 != 1 by apply: nt_sUs usv1P.
have nt_s3: s3 != 1 by apply: nt_sUs usv3P.
have{sUsXp} Ds2p: s2def (w1 ^+ p) (w2 ^+ p) (w3 ^+ p).
  have [/sUsXp-usv1pP /sUsXp-usv2pP /sUsXp-usv3pP] := And3 usv1P usv2P usv3P.
  rewrite expUMp ?groupV // !expgVn in usv1pP usv2pP.
  rewrite !(=^~ conjXg _ _ p, expUMp) ?groupV -1?[t]expg1 ?nUtn ?nUtVn //.
  apply: Ds2 usv1pP usv2pP usv3pP => //.
  by rewrite !psiX // -!Frobenius_autE -rmorphD Dab rmorph_nat.
have{Ds2} Ds2: s2def w1 w2 w3 by apply: Ds2 usv1P usv2P usv3P.
wlog [Uw1 Uw2 Uw3]: w1 w2 w3 Ds2p Ds2 / [/\ w1 \in U, w2 \in U & w3 \in U].
  by move/(_ w1 w2 w3)->; rewrite ?(nUtVn, nUtVn 1%N, nUtn 1%N, in_group).
have{Ds2p} Dw3p: (w2 ^- p * w1 ^- p.-1 ^ s3 * w2) ^ t ^+ 2 = w3 ^+ p.-1 ^ s1^-1.
  rewrite -[w1 ^+ _](mulKg w1) -[w3 ^+ _](mulgK w3) -expgS -expgSr !prednK //.
  rewrite -(canLR (mulKg _) Ds2p) -(canLR (mulKg _) Ds2) 6!invMg !invgK.
  by rewrite mulgA mulgK [2]lock /conjg !mulgA mulVg mul1g mulgK.
have w_id w: w \in U -> w ^+ p.-1 == 1 -> w = 1.
  by move=> Uw /eqP/(canRL_in (expgK _) Uw)->; rewrite ?expg1n ?oU.
have{Uw3} Dw3: w3 = 1.
  apply: w_id => //; have:= @not_splitU s1^-1^-1 s1^-1 (w3 ^+ p.-1).
  rewrite !groupV mulVg eqxx andbT {2}invgK (negPf nt_s1) groupX //= => -> //.
  have /tiH_P1 <-: t ^+ 2 \in P1^#.
    rewrite 2!inE groupX // andbT -order_dvdn gtnNdvd // orderJ.
    by rewrite odd_gt2 ?order_gt1 // orderE defP0 (oddSg sP0P).
  by rewrite -mulgA -conjgE inE -{2}Dw3p memJ_conjg !in_group ?Hs1 // sUH.
have{Dw3p} Dw2p: w2 ^+ p.-1 = w1 ^- p.-1 ^ s3.
  apply/(mulIg w2)/eqP; rewrite -expgSr prednK // eq_mulVg1 mulgA.
  by rewrite (canRL (conjgK _) Dw3p) Dw3 expg1n !conj1g.
have{Uw1} Dw1: w1 = 1.
  apply: w_id => //; have:= @not_splitU s3^-1 s3 (w1 ^- p.-1).
  rewrite mulVg (negPf nt_s3) andbF -mulgA -conjgE -Dw2p !in_group //=.
  by rewrite eqxx andbT eq_invg1 /= => ->.
have{w1 w2 w3 Dw1 Dw3 w_id Uw2 Dw2p Ds2} Ds2: t * s2^-1 * t = s3 * t ^+ 2 * s1.
  by rewrite Ds2 Dw3 [w2]w_id ?mulg1 ?Dw2p ?Dw1 ?mul1g // expg1n invg1 conj1g.
have /centsP abP0: abelian P0 by rewrite -defP0 cycle_abelian.
have QP0ys := memJ_norm y (subsetP (commg_normr P0 Q) _ _).
have{QP0ys} memQP0 := (QP0ys, groupV, groupM); have nQ_P0 := subsetP nQP0.
have sQP0_Q: [~: Q, P0] \subset Q by rewrite commg_subl.
have /centsP abQP0 := abelianS sQP0_Q (abelem_abelian abelQ).
have{s2def} Ds312: s3 * s1 * s2 = 1.
  apply/set1P; rewrite -set1gE -(coprime_TIg coQP) inE.
  rewrite coset_idr ?(subsetP sP0P) ?nQ_P0 ?groupM //.
  rewrite -mulgA -[s2](mulgK s) [_ * s]abP0 // -[s2](mulKVg s).
  rewrite -!mulgA [s * _]mulgA [s1 * _]mulgA [s1 * _]abP0 ?groupM //.
  rewrite 2!(mulgA s3) [s^-1 * _]mulgA !(morphM, morphV) ?nQ_P0 ?in_group //=.
  have ->: coset Q s = coset Q t by rewrite coset_kerl ?groupV ?coset_kerr.
  have nQt: t \in 'N(Q) by rewrite -(conjGid Qy) normJ memJ_conjg nQ_P0.
  rewrite -morphV // -!morphM ?(nQt, groupM) ?groupV // ?nQ_P0 //= -Ds2.
  by rewrite 2!mulgA mulgK mulgKV mulgV morph1.
pose x := (y ^ s3)^-1 * y ^ s^-1 * (y ^ (s * s1)^-1)^-1 * y.
have{abP0} Dx: x ^ s^-1 = x.
  rewrite 3!conjMg !conjVg -!conjgM -!invMg (mulgA s) -(expgS _ 1).
  rewrite [x]abQP0 ?memQP0 // [rhs in y * rhs]abQP0 ?memQP0 //.
  apply/(canRL (mulKVg _)); rewrite 4!mulgA; congr (_ * _).
  rewrite [RHS]abQP0 ?memQP0 //; apply/(canRL (mulgK _))/eqP.
  rewrite -3!mulgA [rhs in y^-1 * rhs]abQP0 ?memQP0 // -eq_invg_sym eq_invg_mul.
  apply/eqP; transitivity (t ^+ 2 * s1 * (t^-1 * s2 * t^-1) * s3); last first.
    by rewrite -[s2]invgK -!invMg mulgA Ds2 -(mulgA s3) invMg mulKVg mulVg.
  rewrite (canRL (mulKg _) Ds312) -2![_ * t^-1]mulgA.
  have Dt1 si: si \in P0 -> t^-1 = (s^-1 ^ si) ^ y.
    by move=> P0si; rewrite {2}/conjg -conjVg -(abP0 si) ?groupV ?mulKg.
  by rewrite {1}(Dt1 s1) // (Dt1 s3^-1) ?groupV // -conjXg /conjg !{1}gnorm.
have{Dx memQP0} Dx1: x = 1.
  apply/set1P; rewrite -set1gE; have [_ _ _ <-] := dprodP defQ.
  rewrite setIAC (setIidPr sQP0_Q) inE -{2}defP0 -cycleV cent_cycle.
  by rewrite (sameP cent1P commgP) commgEl Dx mulVg eqxx !memQP0.
pose t1 := s1 ^ y; pose t3 := s3 ^ y.
have{x Dx1} Ds13: s1 * (t * t1)^-1 = (t3 * t)^-1 * s3.
  by apply/eqP; rewrite eq_sym eq_mulVg1 invMg invgK -Dx1 /x /conjg !gnorm.
suffices Ds1: s1 = s^-1.
  rewrite -(canLR (mulKg _) (canRL (mulgKV _) Dusv1)) Ds1 Duv1.
  by rewrite !invMg invgK /conjg !gnorm.
have [_ _ /trivgPn[u Uu nt_u] _ _] := Frobenius_context frobH.
apply: (conjg_inj y); apply: contraNeq nt_u.
rewrite -/t1 conjVg -/t eq_mulVg1 -invMg => nt_tt1.
have Hu := sUH u Uu; have P1tt1: t * t1 \in P1 by rewrite groupM ?memJ_conjg.
have /tiH_P1 defU: (t * t1)^-1 \in P1^# by rewrite 2!inE nt_tt1 groupV.
suffices: (u ^ s1) ^ (t * t1)^-1 \in U.
  rewrite -mem_conjg nUP1 // conjgE mulgA => /(not_splitU _ _ Uu).
  by rewrite groupV (negPf nt_s1) andbF mulVg eqxx andbT /= => /(_ _ _)/eqP->.
rewrite -defU inE memJ_conjg -conjgM Ds13 conjgM groupJ ?(groupJ _ Hs1) //.
by rewrite sUH // -mem_conjg nUP1 // groupM ?memJ_conjg.
Qed.

End AppendixC3.

Fact BGappendixC_inner_subproof : (p <= q)%N.
Proof.
have [y QP0y nUP0y] := nU_P0QP0.
by apply: Einv_gt1_le_pq E_gt1; apply: BGappendixC3_Ediv nUP0y.
Qed.

End ExpandHypotheses.

(* This is B & G, Appendix C, Theorem C. *)
Theorem prime_dim_normed_finField : (p <= q)%N.
Proof.
apply: wlog_neg; rewrite -ltnNge => ltqp.
have [F sigma /isomP[inj_sigma im_sigma] defP0] := fieldH.
case=> sigmaU inj_sigmaU sigmaJ.
have oF: #|F| = (p ^ q)%N by rewrite -cardsT -im_sigma card_injm.
have charFp: p \in [char F] := card_finCharP oF pr_p.
have sP0P: P0 \subset P by rewrite -defP0 subsetIl.
pose s := invm inj_sigma 1%R.
have sigma_s: sigma s = 1%R by rewrite invmK ?im_sigma ?inE.
have{defP0} defP0: <[s]> = P0.
  by rewrite -morphim_cycle /= ?im_sigma ?inE // morphim_invmE.
exact: BGappendixC_inner_subproof defP0 sigmaJ.
Qed.

End AppendixC.