Merge pull request #68 from math-comp/semi-poly

Adapt to math-comp/math-comp#1395

Author: proux01

theories/BGappendixC.v

@@ -237,7 +237,7 @@ 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 := [set x : galF | Nm x == 1 & Nm (2 - x) == 1].
 
 Let E_1 : 1 \in E.
 Proof. by rewrite !inE -addrA subrr addr0 galNorm1 eqxx. Qed.
@@ -246,7 +246,7 @@ Proof. by rewrite !inE -addrA subrr addr0 galNorm1 eqxx. Qed.
 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.
+pose tau (x : F) := (2 - x)^-1.
 have Etau x: x \in E -> tau x \in E.
   rewrite inE => Ex; rewrite Einv (imset_f (fun y => y^-1)) //.
   by rewrite inE andbC opprD addNKr opprK.
@@ -376,7 +376,7 @@ have [q_gt4 | q_le4] := ltnP 4 q.
     by rewrite ltn_sub2l ?(ltn_exp2l 0) // prime_gt1.
   rewrite -mulrDr -natrX -expnM muln2 -subn1 doubleB -addnn -addnBA // subn2.
   rewrite expnD natrM -oP ler_wpM2l ?ler0n //.
-  apply: le_trans (_ : 2%:R * sqrtC #|P|%:R <= _).
+  apply: le_trans (_ : 2 * sqrtC #|P|%:R <= _).
     rewrite mulrDl mul1r lerD2l -(@expr_ge1 _ 2) ?(ltW sqrtP_gt0) // sqrtCK.
     by rewrite oP natrX expr_ge1 ?ler0n ?ler1n.
   rewrite -ler_sqr ?rpredM ?rpred_nat ?qualifE ?(ltW sqrtP_gt0) //.
@@ -385,10 +385,14 @@ have [q_gt4 | q_le4] := ltnP 4 q.
   by rewrite ?leq_exp2l // !doubleS !ltnS -addnn leq_addl.
 have q3: q = 3%N 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 /= !hornerE; apply/val_inj.
-have fc2 c: (f c).[2%:R] = 1.
-  by rewrite !(subrr, hornerE) /= addrK; apply/val_inj.
+pose f (c : 'F_p) : {poly 'F_p} := 'X * ('X - 2%:P) * ('X - c%:P) + ('X - 1).
+(* TODO when requiring mathcomp >= 2.4.0, the following three lines
+   can be simplified to
+     have fc0 c: (f c).[0] = -1 by rewrite !hornerE.
+     have fc2 c: (f c).[2] = 1 by rewrite !(subrr, hornerE) /= addrK.
+   c.f. https://github.com/math-comp/odd-order/pull/68#discussion_r2030878922 *)
+have fc0 c: (f c).[0] = -1 by rewrite !hornerE //= !hornerE.
+have fc2 c: (f c).[2] = 1 by rewrite !(subrr, hornerE) /= addrK; apply/val_inj.
 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].
@@ -400,7 +404,7 @@ have /existsP[c nz_fc]: [exists c, ~~ [exists d, root (f c) d]].
   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%N.
+have sz_fc_lhs: size ('X * ('X - 2%:P) * ('X - c%:P)) = 4%N.
   by rewrite !(size_mul, =^~ size_poly_eq0) ?size_polyX ?size_XsubC.
 have sz_fc: size (f c) = 4%N by rewrite size_addl ?size_XsubC sz_fc_lhs.
 have irr_fc: irreducible_poly (f c) by apply: cubic_irreducible; rewrite ?sz_fc.
@@ -448,7 +452,7 @@ exists a; rewrite !inE; apply/and3P; split.
     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.
+apply/eqP; transitivity (fcF.[inF 2]); last by rewrite horner_map fc2 rmorph1.
 rewrite DfcF horner_prod; apply: eq_bigr => beta _.
 by rewrite hornerXsubC rmorphB !rmorph_nat.
 Qed.
@@ -615,7 +619,7 @@ suffices EpsiV a: a \in U -> psi a \in E -> psi (a^-1 ^ t ^+ 3) \in E.
   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.
+move=> Ua Ea; have{Ea} [b Ub Dab]: exists2 b, b \in U & psi a + psi b = 2.
   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. *)

theories/BGsection14.v

@@ -1326,7 +1326,7 @@ Theorem Ptype_embedding M K :
                 {in Kstar^#, forall y, 'C_Mstar[y] = Z}
               & {in K^# & Kstar^#, forall x y, 'C[x * y] = Z}]
 & [/\ (*e*) [/\ normedTI Zhat G Z, {in ~: M, forall g, [disjoint Zhat & M :^ g]}
-              & (#|G|%:R / 2%:R < #|class_support Zhat G|%:R :> rat)%R ],
+              & (#|G|%:R / 2 < #|class_support Zhat G|%:R :> rat)%R ],
       (*f*) M \in 'M_'P2 /\ prime #|K| \/ Mstar \in 'M_'P2 /\ prime #|Kstar|,
       (*g*) {in 'M_'P, forall H, gval H \in M :^: G :|: Mstar :^: G}
     & (*h*) M^`(1) ><| K = M]].
@@ -1768,7 +1768,7 @@ have hallKs: \sigma(M).-Hall(Mstar) Ks.
     by rewrite subsetI sYMs (subset_trans sYMstar) ?gFnorm.
   rewrite subsetI -{1}defKs_star subsetIl.
   by rewrite (subset_trans (pHall_sub hallK)) ?gFnorm.
-have oTGgt_g2: (g / 2%:R < #|TG|%:R)%R.
+have oTGgt_g2: (g / 2 < #|TG|%:R)%R.
   rewrite oTG big_setU1 //= /n defMNX big_set1 cards1 mulrC mul1r.
   rewrite ltr_pM2r ?(ltr_nat _ 0) ?cardG_gt0 //  /k_ K0 -defKs.
   rewrite /z -defZ -(dprod_card defNK) natrM invfM opprD.
@@ -1867,15 +1867,15 @@ split=> // [||H PmaxH].
 have [maxH _] := setDP PmaxH.
 have{maxH}[L hallL] := Hall_exists \kappa(H) (mmax_sol maxH).
 pose Ls := 'C_(H`_\sigma)(L); pose S := (L <*> Ls) :\: (L :|: Ls).
-have{IHn} oSGgt_g2: (g / 2%:R < #|class_support S G|%:R)%R.
+have{IHn} oSGgt_g2: (g / 2 < #|class_support S G|%:R)%R.
   have [|nTG_leS] := ltnP #|class_support S G| nTG.
     by case/IHn=> // Sstar _ [_ _ _ _ [[_ _ -> //]]].
   apply: lt_le_trans oTGgt_g2 _; rewrite ler_nat /TG -defZhat.
   exact: leq_trans leTGn nTG_leS.
 have{oSGgt_g2 oTGgt_g2} meetST: ~~ [disjoint TG & class_support S G].
   rewrite -leq_card_setU; apply: contraTneq (leqnn #|G|) => tiTGS.
   rewrite -ltnNge -(ltr_nat rat) -/g.
-  rewrite -{1}[g](@divfK _ 2%:R) // mulr_natr.
+  rewrite -{1}[g](@divfK _ 2) // mulr_natr.
   apply: lt_le_trans (ltrD oTGgt_g2 oSGgt_g2) _.
   by rewrite -natrD -tiTGS ler_nat cardsT max_card.
 have{meetST} [x Tx [a Sx]]: exists2 x, x \in T & exists a, x \in S :^ a.

theories/PFsection1.v

@@ -140,8 +140,7 @@ by rewrite cfdotZl [d in _ * d]cfdotC Cmu rmorph0 mulr0.
 Qed.
 
 Let vchar_isometry_base3 f f' : 
-  f \in 'Z[irr G, G^#] -> '[f]_G = 2%:R ->
-  f' \in 'Z[irr G, G^#] -> '[f']_G = 2%:R ->
+  f \in 'Z[irr G, G^#] -> '[f]_G = 2 -> f' \in 'Z[irr G, G^#] -> '[f']_G = 2 ->
   '[f, f'] = 1 ->
    exists es : _ * bool, let: (i, j, k, epsilon) := es in
      [/\  f = (-1) ^+ epsilon *: ('chi_j - 'chi_i),
@@ -206,7 +205,7 @@ pose F i j := chi i - chi j.
 have DF i j : F i j =  F i 0 - F j 0 by rewrite /F opprB addrA subrK.
 have ZF i j: F i j \in 'Z[Chi, L].
   by rewrite zchar_split rpredB ?mem_zchar // DF memvB // /F !chiE.
-have htau2 i j: i != j -> '[tau (F i j)] = 2%:R.
+have htau2 i j: i != j -> '[tau (F i j)] = 2.
   rewrite iso_tau // cfnormB -cfdotC !dot_chi !eqxx eq_sym => /negbTE->.
   by rewrite -!natrD subr0.
 have htau1 i j: j != 0 -> j != i -> i != 0 -> '[tau (F i 0), tau (F j 0)] = 1.

theories/PFsection10.v

@@ -312,8 +312,7 @@ Local Notation Zalpha_tau := vchar_Dade_FTtype345_bridge.
 (* This covers the last paragraph in the proof of (10.5); it's isolated here  *)
 (* because it is reused in the proof of (10.10) and (11.8).                   *)
 
-Lemma norm_FTtype345_bridge i j :
-  j != 0 -> '[(alpha_ i j)^\tau] = 2%:R + n ^+ 2.
+Lemma norm_FTtype345_bridge i j : j != 0 -> '[(alpha_ i j)^\tau] = 2 + n ^+ 2.
 Proof.
 move=> nz_j; rewrite Dade_isometry ?alpha_on // cfnormBd ?cfnormZ; last first.
   by rewrite cfdotZr cfdotBl cfdotZl !o_mu2_zeta !(mulr0, subr0).
@@ -337,7 +336,7 @@ have [[_ Ddelta _ Nn] [[Itau1 Ztau1] _]] := (FTtype345_constants, cohS1).
 have [|z Zz defY] := zchar_expansion _ S1_Y.
   rewrite map_inj_in_uniq; first by case: sS10.
   by apply: sub_in2 (Zisometry_inj Itau1); apply: mem_zchar.
-have nX_2: '[X] = 2%:R.
+have nX_2: '[X] = 2.
   apply: (addrI '[Y]); rewrite -cfnormDd // addrC -Dalpha norm_alpha //.
   by rewrite addrC nY_n2.
 have Z_X: X \in 'Z[irr G].
@@ -417,7 +416,7 @@ have al_ij_zeta_s: '[al_ij^\tau, zeta^*^\tau1] = a.
 have Zal_ij: al_ij^\tau \in 'Z[irr G] by apply: Zalpha_tau.
 have Za: a \in Num.int.
   by rewrite rpredD ?(intr_nat Nn) ?Cint_cfdot_vchar ?Ztau1 ?(mem_zchar Szeta).
-have{al_ij_zeta_s} ub_da2: (d ^ 2)%:R * a ^+ 2 <= (2%:R + n ^+ 2) * w1%:R.
+have{al_ij_zeta_s} ub_da2: (d ^ 2)%:R * a ^+ 2 <= (2 + n ^+ 2) * w1%:R.
   have [k nz_k j'k]: exists2 k, k != 0 & k != j.
     have:= w2gt2; rewrite -nirrW2 (cardD1 0) (cardD1 j) !inE nz_j !ltnS lt0n.
     by case/pred0Pn=> k /and3P[]; exists k.
@@ -431,7 +430,7 @@ have{al_ij_zeta_s} ub_da2: (d ^ 2)%:R * a ^+ 2 <= (2%:R + n ^+ 2) * w1%:R.
     rewrite !(cfdot_prTIirr_red pddM) cfdotC o_mu_zeta conjC0 !mulr0 mulr1.
     by rewrite 2![_ == k](negPf _) 1?eq_sym // mulr0 -mulrN opprB !subr0 add0r.
   have ZSmuk: mu_ k \in 'Z[calS] by rewrite mem_zchar ?calSmu.
-  have <-: '[al_ij^\tau] * '[(mu_ k)^\tau1] = (2%:R + n ^+ 2) * w1%:R.
+  have <-: '[al_ij^\tau] * '[(mu_ k)^\tau1] = (2 + n ^+ 2) * w1%:R.
     by rewrite Itau1 // cfdot_prTIred eqxx mul1n norm_alpha.
   by rewrite -intr_normK ?cfCauchySchwarz // Cint_cfdot_vchar // Ztau1.
 suffices a0 : a = 0.
@@ -460,7 +459,7 @@ apply: le_lt_trans (_ : n ^+ 2 * (w1%:R - 1) < _).
 rewrite -(ltr_pM2l (gt0CG W1)) -/w1 2!mulrBr mulr1 mulrCA -exprMn.
 rewrite mulrDr ltrBlDl addrCA -mulrDr mulrCA mulrA -ltrBlDl.
 rewrite -mulrBr mulNr opprK divfK ?neq0CG // mulr_natr addrA subrK -subr_sqr.
-rewrite sqrr_sign mulrC [_ + 2%:R]addrC (lt_le_trans _ ub_da2) //.
+rewrite sqrr_sign mulrC [_ + 2]addrC (lt_le_trans _ ub_da2) //.
 apply: lt_le_trans (ler_wpM2l (ler0n _ _) a2_ge1).
 by rewrite mulr1 ltrBlDl -mulrS -natrX ltC_nat.
 Qed.
@@ -777,14 +776,14 @@ rewrite cards1 natrB ?addn_gt0 ?cardG_gt0 // addnC natrD -addrA mulrDl mulrBl.
 rewrite {1}mulnC !natrM !invfM !mulVKf ?natrG_neq0 // opprD -addrA lerD2l.
 rewrite mul1r -{1}[_^-1]mul1r addrC lerNr [- _]opprB -!mulrBl.
 rewrite -addrA -opprD ler_pdivlMr; last by rewrite natrG_gt0.
-apply: le_trans (_ : 1 - (3%:R^-1 + 7%:R^-1) <= _); last first.
+apply: le_trans (_ : 1 - (3^-1 + 7^-1) <= _); last first.
   rewrite lerD2l lerN2.
   rewrite lerD // lef_pV2 ?qualifE/= ?gt0CG ?ltr0n ?ler_nat //.
   have notStype5: FTtype S != 5%N by rewrite (eqP Stype2).
   have frobUW2 := Ptype_compl_Frobenius maxS StypeP notStype5.
   apply: leq_ltn_trans (ltn_odd_Frobenius_ker frobUW2 (mFT_odd _)).
   by rewrite (leq_double 3).
-apply: le_trans (_ : 2%:R^-1 <= _); last by rewrite -!CratrE; compute.
+apply: le_trans (_ : 2^-1 <= _); last by rewrite -!CratrE; compute.
 rewrite mulrAC ler_pdivrMr 1?gt0CG // ler_pdivlMl ?ltr0n //.
 rewrite -!natrM ler_nat mulnA -(Lagrange (normal_sub nsM''M')) mulnC leq_mul //.
   by rewrite subset_leq_card //; have [_ _ _ []] := MtypeP.
@@ -964,7 +963,7 @@ have [j nz_j] := has_nonprincipal_irr ntW2.
 have [Dmu2_1 Ddelta_ lt1d Nn] := FTtype345_constants.
 have{lt1d} [defS szS1 Dd Ddel Dn]:
         [/\ perm_eq calS (S1 ++ S2), size S1 = (p ^ 2 - 1) %/ w1,
-            d = p, delta = -1 & n = 2%:R].
+            d = p, delta = -1 & n = 2].
 - pose X_ (S0 : seq 'CF(M)) := [set s | 'Ind[M, H] 'chi_s \in S0].
   pose sumX_ cS0 := \sum_(s in X_ cS0) 'chi_s 1%g ^+ 2.
   have defX1: X_ S1 = Iirr_kerD H H H'.
@@ -1076,17 +1075,17 @@ have Dalpha i (al_ij := alpha_ i j) :
       by rewrite Da_z' // intr_normK.
     rewrite big_tnth sumr_const card_ord size_rem ?map_f // size_map.
     by rewrite mulr_natl subn1.
-  have{lb_n2alij} ub_a2: (size S1)%:R * a ^+ 2 <= 2%:R * a * n + 2%:R.
+  have{lb_n2alij} ub_a2: (size S1)%:R * a ^+ 2 <= 2 * a * n + 2.
     rewrite norm_alpha // addrC sqrrB !addrA lerD2r in lb_n2alij.
     rewrite mulr_natl -mulrSr lerBlDl subn1 in lb_n2alij.
     by rewrite -mulrA !mulr_natl; case: (S1) => // in S1zeta lb_n2alij *.
-  have{ub_a2} ub_8a2: 8%:R * a ^+ 2 <= 4%:R * a + 2%:R.
+  have{ub_a2} ub_8a2: 8 * a ^+ 2 <= 4 * a + 2.
     rewrite mulrAC Dn -natrM in ub_a2; apply: le_trans ub_a2.
     rewrite -intr_normK // ler_wpM2r ?exprn_ge0 ?normr_ge0 // leC_nat szS1.
     rewrite (subn_sqr p 1) def_p_w1 subnK ?muln_gt0 // mulnA mulnK // mulnC.
     by rewrite -subnDA -(mulnBr 2%N _ 1%N) mulnA (@leq_pmul2l 4 2) ?ltn_subRL.
-  have Z_4a1: 4%:R * a - 1%:R \in Num.int by rewrite rpredB ?rpredM ?rpred_nat.
-  have{ub_8a2} ub_4a1: `|4%:R * a - 1| < 3%:R.
+  have Z_4a1: 4 * a - 1 \in Num.int by rewrite rpredB ?rpredM ?rpred_nat/=.
+  have{ub_8a2} ub_4a1: `|4 * a - 1| < 3.
     rewrite -ltr_sqr ?rpred_nat ?qualifE/= ?normr_ge0 // -natrX intr_normK //.
     rewrite sqrrB1 exprMn -natrX -mulrnAl -mulrnA (natrD _ 8 1) ltrD2r.
     rewrite (natrM _ 2 4) (natrM _ 2 8) -!mulrA -mulrBr ltr_pM2l ?ltr0n //.

theories/PFsection11.v

@@ -227,7 +227,7 @@ Lemma bounded_proper_coherent H1 :
     (#|HU : H1| <= 2 * q * #|U : C| + 1)%N.
 Proof.
 move=> nsH1_M psH1_M' cohH1; have [nsHHU _ _ _ _] := sdprod_context defHU.
-suffices: #|HU : H1|%:R - 1 <= 2%:R * #|M : HC|%:R * sqrtC #|HC : HC|%:R :> algC.
+suffices: #|HU : H1|%:R - 1 <= 2 * #|M : HC|%:R * sqrtC #|HC : HC|%:R :> algC.
   rewrite indexgg sqrtC1 mulr1 -leC_nat natrD -lerBlDr -mulnA natrM.
   congr (_ <= _ * _%:R); apply/eqP; rewrite -(eqn_pmul2l (cardG_gt0 HC)).
   rewrite Lagrange ?normal_sub // mulnCA -(dprod_card defHC) -mulnA mulnC.
@@ -884,18 +884,18 @@ have tau_alpha i: tau (alpha_ i j) = eta_ i j - eta_ i 0 - n *: zeta1.
     rewrite cfRes_cfun1 !cfdotBl deltaZ !cfdotZl -!/(mu2_ 0 _).
     rewrite -(prTIirr00 ptiWM) !cfdot_prTIirr cfdotC omu2S1 // conjC0 mulr0.
     by rewrite (negPf nz_j1) add0r subr0 subrr rpred0.
-  have nY: '[Y] = n * a * (a - 2%:R) + n ^+ 2. (* Resuming step (11.8.2). *)
+  have nY: '[Y] = n * a * (a - 2) + n ^+ 2. (* Resuming step (11.8.2). *)
     rewrite defY cfnormD cfnormN !cfnormZ cfdotNr cfdotZr.
     rewrite cfnorm_map_orthonormal // -Dn Itau1 ?mem_zchar ?n1S1 // mulr1.
     rewrite scaler_sumr cfproj_sum_orthonormal // rmorphN addrAC.
     rewrite Dn rmorphM/= !intr_normK ?rpred_nat // !rmorph_nat conj_intr // -Dn.
     by rewrite -mulr2n mulrC mulrA -[in LHS]mulr_natr mulNr -mulrBr.
-  have{a_even} Da: (a == 0) || (a == 2%:R). (* Second part of (11.8.2). *)
+  have{a_even} Da: (a == 0) || (a == 2). (* Second part of (11.8.2). *)
     suffices (b := a - 1): b ^+ 2 == 1.
       by rewrite -!(can_eq (subrK 1) a) add0r addrK orbC -eqf_sqr expr1n.
     have S1gt0: (0 < size S1)%N by case: (S1) S1zeta.
     have: n * b ^+ 2 <= n *+ 3.
-      have: 2%:R + n <= n *+ 3 by rewrite addrC lerD2l lerMn2r Dn ler1n.
+      have: 2 + n <= n *+ 3 by rewrite addrC lerD2l lerMn2r Dn ler1n.
       apply: le_trans; rewrite sqrrB1 -(mulr_natr a) -mulrBr mulrDr mulrA mulr1.
       rewrite lerD2r -(lerD2r (n ^+ 2 + '[X])) !addrA -nY -cfnormDd //.
       by rewrite -Dphi norm_FTtype345_bridge ?S1_1 // lerDl cfnorm_ge0.

theories/PFsection12.v

@@ -982,7 +982,7 @@ have norm_alpha: '[tauL_H alpha] = e%:R + 1.
   rewrite Dade_isometry ?(cfInd1_sub_lin_on _ Schi) ?De //.
   rewrite cfnormBd; last by rewrite cfdotC (seqInd_ortho_Ind1 _ _ Schi) ?conjC0.
   by rewrite cfnorm_Ind_cfun1 // De irrWnorm.
-pose h := #|H|; have ub_a: a ^+ 2 * ((h%:R - 1) / e%:R) - 2%:R * a <= e%:R - 1.
+pose h := #|H|; have ub_a: a ^+ 2 * ((h%:R - 1) / e%:R) - 2 * a <= e%:R - 1.
   rewrite -[h%:R - 1](mulKf (neq0CiG L H)) -sum_seqIndC1_square // De -/calS.
   rewrite -[lhs in lhs - 1](addrK 1) -norm_alpha -[tauL_H _](subrK 1).
   rewrite cfnormDd; last by rewrite cfdotBl tau_alpha_1 cfnorm1 subrr.
@@ -1002,7 +1002,7 @@ have [pr_p p_dv_M]: prime p /\ p %| #|M|.
   by rewrite mem_primes => /and3P[].
 have odd_p: odd p by rewrite (dvdn_odd p_dv_M) ?mFT_odd.
 have pgt2: (2 < p)%N := odd_prime_gt2 odd_p pr_p.
-have ub_e: e%:R <= (p%:R + 1) / 2%:R :> algC.
+have ub_e: e%:R <= (p%:R + 1) / 2 :> algC.
   rewrite ler_pdivlMr ?ltr0n // -natrM -mulrSr leC_nat muln2.
   have [b e_dv_pb]: exists b : bool, e %| (b.*2 + p).-1.
     by have [_ /orP[]] := Ecyclic_le_p; [exists false | exists true].
@@ -1013,7 +1013,7 @@ have ub_e: e%:R <= (p%:R + 1) / 2%:R :> algC.
 have lb_h: p%:R ^+ 2 <= h%:R :> algC.
   rewrite -natrX leC_nat dvdn_leq ?pfactor_dvdn ?cardG_gt0 //.
   by rewrite -prankP0 (leq_trans (p_rankS p sP0H)) ?p_rank_le_logn.
-have{ub_e} ub_a: p.-1.*2%:R * a ^+ 2 - 2%:R * a <= p.-1%:R / 2%:R :> algC.
+have{ub_e} ub_a: p.-1.*2%:R * a ^+ 2 - 2 * a <= p.-1%:R / 2 :> algC.
   apply: le_trans (le_trans ub_a _); last first.
     rewrite -subn1 -subSS natrB ?ltnS ?prime_gt0 // mulrSr mulrBl.
     by rewrite divff ?pnatr_eq0 ?lerD2r.
@@ -1026,11 +1026,11 @@ have a0: a = 0.
   apply: contraTeq ub_a => nz_a; rewrite lt_geF // ltr_pdivrMr ?ltr0n //.
   rewrite mulrC -{1}mulr_natl -muln2 natrM -mulrA mulrBr mulrCA ltrBrDl.
   rewrite -ltrBrDr -mulrBr mulr_natl mulrA -expr2 -exprMn.
-  apply: lt_le_trans (_ : 2%:R * ((a *+ 2) ^+ 2 - 1) <= _); last first.
+  apply: lt_le_trans (_ : 2 * ((a *+ 2) ^+ 2 - 1) <= _); last first.
     rewrite (mulr_natl a 2) ler_wpM2r // ?subr_ge0.
       by rewrite sqr_intr_ge1 ?rpredMn // mulrn_eq0.
     by rewrite leC_nat -subn1 ltn_subRL.
-  rewrite -(@ltr_pM2l _ 2%:R) ?ltr0n // !mulrA -expr2 mulrBr -exprMn mulr1.
+  rewrite -(@ltr_pM2l _ 2) ?ltr0n // !mulrA -expr2 mulrBr -exprMn mulr1.
   rewrite -natrX 2!mulrnAr -[in rhs in _ < rhs]mulrnAl -mulrnA.
   rewrite ltrBrDl -ltrBrDr -(ltrD2r 1) -mulrSr -sqrrB1.
   rewrite -intr_normK ?rpredB ?rpredM ?rpred_nat ?rpred1 //.
@@ -1228,7 +1228,7 @@ have{lb_psiM lb_psiL ub_rhoML ubM} ubK: (#|K / K'|%g < 4)%N.
     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 <= _).
+  apply: le_trans (_ : (1 + 2^-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 //.