diff --git a/theories/BGappendixC.v b/theories/BGappendixC.v
index e6b3085..efd960d 100644
--- a/theories/BGappendixC.v
+++ b/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. *)
diff --git a/theories/BGsection14.v b/theories/BGsection14.v
index 22d4bc3..20c9569 100644
--- a/theories/BGsection14.v
+++ b/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,7 +1867,7 @@ 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.
@@ -1875,7 +1875,7 @@ have{IHn} oSGgt_g2: (g / 2%:R < #|class_support S G|%:R)%R.
 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.
diff --git a/theories/PFsection1.v b/theories/PFsection1.v
index b4073da..168fef8 100644
--- a/theories/PFsection1.v
+++ b/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.
diff --git a/theories/PFsection10.v b/theories/PFsection10.v
index 2f48dcf..d60cd83 100644
--- a/theories/PFsection10.v
+++ b/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 //.
diff --git a/theories/PFsection11.v b/theories/PFsection11.v
index 502be74..6a4d1aa 100644
--- a/theories/PFsection11.v
+++ b/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.
diff --git a/theories/PFsection12.v b/theories/PFsection12.v
index d8fcddb..c5476ef 100644
--- a/theories/PFsection12.v
+++ b/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 //.
diff --git a/theories/PFsection13.v b/theories/PFsection13.v
index 98621a4..3d1d710 100644
--- a/theories/PFsection13.v
+++ b/theories/PFsection13.v
@@ -449,7 +449,7 @@ Let calS1_split1 (tau1 : {additive _ -> _}) zeta1 chi :
       (*b*)
          \sum_(x in H^#) `|chi x| ^+ 2 =
              a ^+ 2 / '[zeta1] * (#|S|%:R - zeta1 1%g ^+ 2 / '[zeta1])
-             - 2%:R * a * (zeta1 1%g * alpha 1%g / '[zeta1])
+             - 2 * a * (zeta1 1%g * alpha 1%g / '[zeta1])
              + (\sum_(x in H^#) `|alpha x| ^+ 2)              
     & (*c*)
          \sum_(x in H^#) `|alpha x| ^+ 2 >= #|P|.-1%:R * alpha 1%g ^+ 2].
@@ -581,7 +581,7 @@ by rewrite raddfZ_int {Zz}//= cfdotZl o_phi_eta ?mulr0.
 Qed.
 
 Let P1_int2_lb (b : algC) :
-  b \in Num.int -> 2%:R * u%:R * b <= #|P|.-1%:R * b ^+ 2.
+  b \in Num.int -> 2 * u%:R * b <= #|P|.-1%:R * b ^+ 2.
 Proof.
 move=> Zb; rewrite -natrM; apply: le_trans (_ : (2 * u)%:R * b ^+ 2 <= _).
   by rewrite ler_wpM2l ?ler0n ?intr_ler_sqr.
@@ -800,7 +800,7 @@ have eta_i1 i: i != 0 -> eta_ i #1 x = eta_ 0 #1 x - 1.
     by rewrite cycTIiso_Ind // (cfun_on0 _ W'x) ?cfInd_on ?subsetT.
   rewrite [alpha]cfCycTI_E linearD !linearB /= !cfunE cycTIiso1 cfun1E inE.
   by rewrite {1}eta_x_0 //= subr0 addrC addr_eq0 opprB.
-have eta11x: eta_ #1 #1 x = - (q%:R)^-1.
+have eta11x: eta_ #1 #1 x = - q%:R^-1.
   rewrite -mulN1r; apply: canRL (mulfK (neq0CG W1)) _.
   transitivity ((-1) ^+ b * sum_eta1 x - 1); last first.
     by rewrite sum_eta1x_0 mulr0 add0r.
@@ -1179,10 +1179,10 @@ Qed.
 Import ssrint.
 (* This is Peterfalvi (13.11). *)
 Let lb_m_cases :
- [/\ (*a*) (q >= 7)%N -> m > 8%:R / 10%:R,
-     (*b*) (q >= 5)%N -> m > 7%:R / 10%:R
+ [/\ (*a*) (q >= 7)%N -> m > 8 / 10,
+     (*b*) (q >= 5)%N -> m > 7 / 10
    & (*c*) q = 3%N ->
-           m > 49%:R / 100 %:R /\ u%:R / c%:R > (p ^ 2).-1%:R / 6%:R :> algC].
+           m > 49 / 100 /\ u%:R / c%:R > (p ^ 2).-1%:R / 6 :> algC].
 Proof.
 pose mkrat b d := fracq (b, d%:Z).
 pose test r b d := 1 - mkrat 1 r.-1 - mkrat 1 (r ^ 2)%N > mkrat b%:Z d.
@@ -1200,12 +1200,12 @@ have lb_m r b d: test r.+2 b d -> (q >= r.+2)%N -> m > b%:R / d%:R.
   by rewrite -(subnKC qgt2) leq_pexp2l // -subn1 ltn_subRL.
 split=> [||q3]; try by apply: lb_m; compute.
 pose d r : algC := (3 ^ r.-1)%:R^-1; pose f r := (r ^ 2)%:R * d r.
-have Dm: m = (1 - d p) / 2%:R.
+have Dm: m = (1 - d p) / 2.
   rewrite mulrBl mul1r -mulrN mulrC /m q3 /= addrAC -addrA natrM invfM -mulrBl.
   rewrite -{1}(ltn_predK pgt2) expnS natrM invfM mulrA.
   by congr (_ + _ / _); apply/eqP; rewrite -!CratrE; compute.
 split; last apply: le_lt_trans gen_lb_uc.
-  apply: lt_le_trans (_ : (1 - d 5%N) / 2%:R <= _).
+  apply: lt_le_trans (_ : (1 - d 5%N) / 2 <= _).
     by rewrite /d -!CratrE; compute.
   rewrite Dm ler_pM2r ?invr_gt0 ?ltr0n // lerD2l lerN2.
   rewrite lef_pV2 ?qualifE/= ?ltr0n ?expn_gt0 // leC_nat leq_pexp2l //=.
@@ -1219,7 +1219,7 @@ rewrite ler_pdivrMr ?ltr0n ?expn_gt0 // mulrAC (expnS 3) (natrM _ 3).
 rewrite mulrA mulfK ?gt_eqF ?ltr0n ?expn_gt0 //.
 rewrite -ler_pdivrMl ?ltr0n // !natrX -exprVn -exprMn.
 rewrite [X in _ * X]mulrS mulrDr mulr1 mulVf ?pnatr_eq0 //.
-apply: le_trans (_ : (3%:R^-1 + 1) ^+ 2 <= _); last by rewrite -!CratrE; reflexivity.
+apply: le_trans (_ : (3^-1 + 1) ^+ 2 <= _); last by rewrite -!CratrE; reflexivity.
 rewrite ler_sqr ?rpredD ?rpred1 ?rpredV ?rpred_nat // lerD2r.
 by rewrite lef_pV2 ?qualifE/= ?ltr0n ?leC_nat.
 Qed.
@@ -1229,9 +1229,9 @@ Let small_m_q3 : m < (q * p)%:R / (q.*2.+1 * p.-1)%:R -> q = 3%N /\ (p >= 5)%N.
 Proof.
 move=> ub_m; have [lb7_m lb5_m _] := lb_m_cases.
 have [p3 | p_neq3] := eqVneq p 3%N.
-  have ub7_m: ~~ (8%:R / 10%:R < m).
+  have ub7_m: ~~ (8 / 10 < m).
     rewrite lt_gtF // (lt_le_trans ub_m) // p3 /=.
-    apply: le_trans (_ : 3%:R / 4%:R <= _); last first.
+    apply: le_trans (_ : 3 / 4 <= _); last first.
       by rewrite -!CratrE; compute.
     rewrite ler_pdivlMr ?ltr0n // mulrAC ler_pdivrMr ?ltr0n ?muln_gt0 //.
     by rewrite -!natrM leC_nat mulnCA mulSn -muln2 -!mulnA leq_addl.
@@ -1241,9 +1241,9 @@ have [p3 | p_neq3] := eqVneq p 3%N.
   have /implyP := lt_trans (lb5_m _) ub_m.
   by rewrite q5 p3 -!CratrE; compute.
 have pge5: (5 <= p)%N by rewrite odd_geq ?mFT_odd // ltn_neqAle eq_sym p_neq3.
-have ub5_m: ~~ (7%:R / 10%:R < m).
+have ub5_m: ~~ (7 / 10 < m).
   rewrite lt_gtF // (lt_le_trans ub_m) //.
-  apply: le_trans (_ : 2%:R^-1 * (1 + 4%:R^-1) <= _); last first.
+  apply: le_trans (_ : 2^-1 * (1 + 4^-1) <= _); last first.
     by rewrite -!CratrE; compute.
   rewrite !natrM invfM mulrACA ler_pM ?divr_ge0 ?ler0n //.
     rewrite ler_pdivrMr ?ler_pdivlMl ?ltr0n // -natrM mul2n leC_nat.
@@ -1291,7 +1291,7 @@ have [_ _ [//|lb_m lb_uc]] := lb_m_cases.
 pose sum3 r : algC := (r.+1 ^ 2)%:R^-1 + r.+1%:R^-1 + 1.
 have [b Dc1] := dvdnP dv_2q_c1; rewrite q3 in Dc1.
 have [b0 | b_gt0] := posnP b; first by rewrite b0 -(subnKC c_gt1) in Dc1.
-have ub3_m r a: (r < p)%N -> (a <= b)%N -> m < 3%:R / (a * 6).+1%:R * sum3 r.
+have ub3_m r a: (r < p)%N -> (a <= b)%N -> m < 3 / (a * 6).+1%:R * sum3 r.
   move=> lb_p lb_b; apply: lt_le_trans ub_m _.
   rewrite !natrM !invfM mulrACA -!mulrA q3 ler_pM2l ?ltr0n //.
   rewrite -(ltn_predK c_gt1) Dc1 ler_pM ?mulr_ge0 ?invr_ge0 ?ler0n //.
@@ -1369,7 +1369,7 @@ have{ub_m} q3: q = 3%N.
 have [[]] := dvdnP u_dv_p2q; rewrite q3; first by rewrite -(subnKC pgt2).
 case=> [|b] Du; first by rewrite oU c1 Du muln1 mul1n.
 have [_ /idPn[]] := lb3_m q3; rewrite c1 divr1 le_gtF //.
-apply: le_trans (_ : (p.-1 ^ 2)%:R / 8%:R <= _).
+apply: le_trans (_ : (p.-1 ^ 2)%:R / 8 <= _).
   rewrite (natrX _ 2 3) exprSr invfM mulrA natrX -expr_div_n -natf_div // divn2.
   by rewrite -natrX Du ler_pdivlMr ?ltr0n // mulrC -natrM leC_nat leq_mul.
 rewrite -!subn1 (subn_sqr p 1) !natrM -!mulrA ler_wpM2l ?ler0n //.
@@ -1920,7 +1920,7 @@ have{} oYeta j: '[Y, eta_ 0 j] = 0.
 have o_eta1s1: '[eta01^*, eta01] = 0.
   rewrite Deta01s cfdot_cycTIiso /= -(inj_eq irr_inj) aut_IirrE.
   by rewrite odd_eq_conj_irr1 ?mFT_odd // irr_eq1 (negPf nzj1).
-rewrite -(lerD2r 2%:R) -natrD -(norm_beta #1) //.
+rewrite -(lerD2r 2) -natrD -(norm_beta #1) //.
 have ->: '[beta_ #1] = '[Gamma - eta01 + 1].
   by rewrite addrK subrK Dade_isometry ?A0beta.
 rewrite addrA cfnormDd ?cfnorm1 ?lerD2r; last first.
@@ -2043,7 +2043,7 @@ have otau1eta: orthogonal (map tau1 calL) (map sigma (irr W)).
     rewrite FT_DadeF_supportE -defA; apply: contra_eqN tiA_PWG => Ax.
     by apply/set0Pn; exists x; rewrite !inE Ax orbC mem_class_support.
   have opsi: '[psi, psi^*] = 0 by apply: seqInd_conjC_ortho (mFT_odd _) _ Lpsi.
-  have n2Psi: '[Psi] = 2%:R.
+  have n2Psi: '[Psi] = 2.
     by rewrite Itau1 ?cfnormBd // cfnorm_conjC ?irrWnorm ?irrL.
   have NC_Psi: (NC Psi < minn q p)%N.
     by rewrite (@leq_ltn_trans 2) ?leq_min ?qgt2 // cycTI_NC_norm ?Ztau1 ?n2Psi.
diff --git a/theories/PFsection14.v b/theories/PFsection14.v
index ac73785..b83ab4e 100644
--- a/theories/PFsection14.v
+++ b/theories/PFsection14.v
@@ -993,7 +993,7 @@ have lb_rho: 1 - pq / k%:R <= '[rho (tau1M psi)].
   rewrite odd_Frobenius_index_ler ?mFT_odd // => -[_ _ [|/(le_trans _)->] //].
   by rewrite lerD2l lerN2 ler_pM2r ?invr_gt0 ?gt0CG // leC_nat.
 have{rho sumG0 sumG0_diff ub_rho lb_rho} []:
-  ~ pq / k%:R + 2%:R / pq + (u * q)%:R^-1 + (v * p)%:R^-1 < p%:R^-1 + q%:R^-1.
+  ~ pq / k%:R + 2 / pq + (u * q)%:R^-1 + (v * p)%:R^-1 < p%:R^-1 + q%:R^-1.
 - rewrite le_gtF // -!addrA -lerBlDl -lerBrDl -(lerD2l 1).
   apply: le_trans {ub_rho lb_rho}(le_trans lb_rho ub_rho) _.
   rewrite /sumG0_diff -!addnA natrD opprD [in leLHS]addrA mulrBr opprB.
@@ -1013,7 +1013,7 @@ have{rho sumG0 sumG0_diff ub_rho lb_rho} []:
   by rewrite addrACA -opprB opprK.
 rewrite -!addrA ler_ltD //; last first.
   pose q2 : algC := (q ^ 2)%:R.
-  apply: lt_le_trans (_ : 2%:R / q2 + (2%:R * q2)^-1 *+ 2 <= _); last first.
+  apply: lt_le_trans (_ : 2 / q2 + (2 * q2)^-1 *+ 2 <= _); last first.
     rewrite addrC -[_ *+ 2]mulr_natl invfM mulVKf ?pnatr_eq0 //.
     rewrite mulr_natl -mulrS -[leLHS]mulr_natl [q2]natrM.
     by rewrite ler_pdivrMr ?mulr_gt0 ?gt0CG // mulKf ?neq0CG ?leC_nat.
diff --git a/theories/PFsection3.v b/theories/PFsection3.v
index d9be5f2..6da0e91 100644
--- a/theories/PFsection3.v
+++ b/theories/PFsection3.v
@@ -493,7 +493,7 @@ have ->: eval_cl m kvs = X.
   rewrite {}defX !big_map; apply: eq_big_seq => kv /clP[_ /eqP->].
   by rewrite scaler_int.
 rewrite -leC_nat -ltC_nat -eqC_nat /=.
-have <-: '[beta] = 3%:R by rewrite Dm // /dot_ref !eqxx.
+have <-: '[beta] = 3 by rewrite Dm // /dot_ref !eqxx.
 have <-: '[X] = norm%:R.
   rewrite {}defX {}/norm cfnorm_sum_orthonormal // {o1Aij oYij sAm}/Aij.
   transitivity (\sum_(kv <- kvs) `|kv.2%:~R : algC| ^+ 2).
@@ -930,7 +930,7 @@ move=> nzi nzj; rewrite alphaE -w_00 !cfdotDl !cfdotNl !cfdot_w.
 by rewrite !eqxx andbT /= (negPf nzi) (negPf nzj) addr0 !subr0.
 Qed.
 
-Let cfnorm_alpha i j : i != 0 -> j != 0 -> '[alpha_ i j] = 4%:R.
+Let cfnorm_alpha i j : i != 0 -> j != 0 -> '[alpha_ i j] = 4.
 Proof.
 move=> nzi nzj; rewrite -[4%N]/(size [:: 1; - w_ i 0; - w_ 0 j; w_ i j]).
 rewrite -cfnorm_orthonormal 3?big_cons ?big_seq1 ?addrA -?alphaE //.
@@ -1679,7 +1679,7 @@ Qed.
 (* Another consequence of (3.8), used in (4.8), (10.5), (10.10) and (11.8). *)
 Lemma eq_signed_sub_cTIiso phi e i j1 j2 :
     let rho := (-1) ^+ e *: (eta_ i j1 - eta_ i j2) in
-    phi \in 'Z[irr G] -> '[phi] = 2%:R -> j1 != j2 ->
+    phi \in 'Z[irr G] -> '[phi] = 2 -> j1 != j2 ->
   {in V, phi =1 rho} -> phi = rho.
 Proof.
 set rho := _ - _; move: phi => phi0 /= Zphi0 n2phi0 neq_j12 eq_phi_rho.
@@ -1687,9 +1687,9 @@ pose phi := (-1) ^+ e *: phi0; pose psi := phi - rho.
 have{eq_phi_rho} psiV0 z: z \in V -> psi z = 0.
   by move=> Vz; rewrite !cfunE eq_phi_rho // !cfunE signrMK subrr.
 have{Zphi0} Zphi: phi \in 'Z[irr G] by rewrite rpredZsign.
-have{n2phi0} n2phi: '[phi] = 2%:R by rewrite cfnorm_sign.
+have{n2phi0} n2phi: '[phi] = 2 by rewrite cfnorm_sign.
 have Zrho: rho \in 'Z[irr G] by rewrite rpredB ?cycTIiso_vchar.
-have n2rho: '[rho] = 2%:R.
+have n2rho: '[rho] = 2.
   by rewrite cfnormBd !cfdot_cycTIiso ?eqxx ?(negPf neq_j12) ?andbF.
 have [oIphi _ Dphi] := dirr_small_norm Zphi n2phi isT.
 have [oIrho _ Drho] := dirr_small_norm Zrho n2rho isT.
diff --git a/theories/PFsection5.v b/theories/PFsection5.v
index a8d249f..be2568f 100644
--- a/theories/PFsection5.v
+++ b/theories/PFsection5.v
@@ -651,7 +651,7 @@ pose Zortho R := all (mem 'Z[irr G]) R && orthonormal R.
 have R chi: {R : 2.-tuple 'CF(G) | (chi \in S) ==> sum_beta chi R && Zortho R}.
   apply: sigW; case Schi: (chi \in S) => /=; last by exists [tuple 0; 0].
   move/(_ _ Schi) in Zbeta; have /irrP[i def_chi] := irrS _ Schi.
-  have: '[beta chi] = 2%:R.
+  have: '[beta chi] = 2.
     rewrite isoL // cfnormBd ?dotSS ?ccS ?eqxx // eq_sym -/(cfReal _).
     by rewrite (negPf (hasPn nrS _ _)).
   case/zchar_small_norm; rewrite ?(zcharW (Ztau _ _)) // => R [oR ZR sumR].
@@ -758,7 +758,7 @@ have oS1sigma phi: phi \in S1 -> orthogonal (R1 phi) (map sigma (irr W)).
     by move=> ? /sSS0/seqInd_vcharW.
   have NCpsi_le2: (NC (tau psi) <= 2)%N.
     have{Itau} [Itau Ztau] := Itau.
-    suff: '[tau psi] <= 2%:R by apply: cycTI_NC_norm; apply: zcharW (Ztau _ _).
+    suff: '[tau psi] <= 2 by apply: cycTI_NC_norm; apply: zcharW (Ztau _ _).
     rewrite Itau // cfnormBd; first by rewrite cfnorm_conjC Dphi cfnorm_irr.
     have /pairwise_orthogonalP[_ -> //] := orthoS; first exact: ccS.
     by rewrite eq_sym (hasPn nrS).
@@ -1124,7 +1124,7 @@ Lemma extend_coherent S1 xi1 chi :
     cfConjC_subset S1 S -> xi1 \in S1 -> chi \in S -> chi \notin S1 ->
     [/\ (*a*) coherent S1 L^# tau,
         (*b*) (xi1 1%g %| chi 1%g)%C
-      & (*c*) 2%:R * chi 1%g * xi1 1%g < \sum_(xi <- S1) xi 1%g ^+ 2 / '[xi]] ->
+      & (*c*) 2 * chi 1%g * xi1 1%g < \sum_(xi <- S1) xi 1%g ^+ 2 / '[xi]] ->
   coherent (chi :: chi^*%CF :: S1) L^# tau.
 Proof.
 move=> ccsS1S S1xi1 Schi notS1chi [[tau1 cohS1] xi1_dv_chi1 ub_chi1].
@@ -1210,7 +1210,7 @@ suffices lam0: lam = 0; last apply: contraFeq lb_2_lam_a => nz_lam.
 rewrite ltr_wpDr ?cfnorm_ge0 // -mulr2n -mulr_natl mulrCA.
 have xi11_gt0: xi1 1%g > 0 by rewrite char1_gt0 ?N_S ?sS1S -?cfnorm_eq0 ?nz_nS1.
 have a_gt0: a > 0 by rewrite -(ltr_pM2r xi11_gt0) mul0r -chi1 char1_gt0.
-apply: le_lt_trans (_ : lam ^+ 2 * (2%:R * a) < _).
+apply: le_lt_trans (_ : lam ^+ 2 * (2 * a) < _).
   by rewrite ler_pM2r ?mulr_gt0 ?ltr0n ?intr_ler_sqr.
 rewrite ltr_pM2l ?(lt_le_trans ltr01) ?sqr_intr_ge1 {lam Zlam nz_lam}//.
 rewrite -(ltr_pM2r xi11_gt0) -mulrA -chi1 -(ltr_pM2r xi11_gt0).
@@ -1528,7 +1528,7 @@ pose mu j := 'chi_j 1%g *: 'chi_i - 'chi_i 1%g *: 'chi_j.
 have ZAmu j: 'chi_j \in calS -> mu j \in 'Z[calS, L^#].
   move=> Sxj; rewrite zcharD1E !cfunE mulrC subrr.
   by rewrite rpredB //= scale_zchar ?sSZS // ?intr_nat ?Cnat_irr1.
-have Npsi j: 'chi_j \in calS -> '[tau1 'chi_j] = 1%:R.
+have Npsi j: 'chi_j \in calS -> '[tau1 'chi_j] = 1.
   by move=> Sxj; rewrite Itau1 ?sSZS ?cfnorm_irr.
 have{Npsi} Dtau1 Sxj := vchar_norm1P (Ztau1 _ (sSZS _ Sxj)) (Npsi _ Sxj).
 have [e [r tau1_chi]] := Dtau1 _ Schi; set eps := (-1) ^+ e in tau1_chi.
@@ -1590,7 +1590,7 @@ have Zphi: phi \in 'Z[irr L, A].
   by rewrite -(setU1K notA1) sub_conjC_vchar // zchar_split irr_vchar.
 have Zphi_tau: phi^\tau \in 'Z[irr G, G^#].
   by rewrite zchar_split Dade_cfun Dade_vchar ?Zphi.
-have norm_phi_tau : '[phi^\tau] = 2%:R.
+have norm_phi_tau : '[phi^\tau] = 2.
   rewrite Dade_isometry ?(zchar_on Zphi) // cfnormB -conjC_IirrE.
   by rewrite !cfdot_irr !eqxx eq_sym (negPf notRchi) add0r rmorph0 subr0.
 have [j [k ne_kj phi_tau]] := vchar_norm2 Zphi_tau norm_phi_tau.
diff --git a/theories/PFsection6.v b/theories/PFsection6.v
index 942d875..fa4eff4 100644
--- a/theories/PFsection6.v
+++ b/theories/PFsection6.v
@@ -80,7 +80,7 @@ Lemma coherent_seqIndD_bound (A B C D : {group gT}) :
   (*a*) [/\ A \proper K, B \subset D, D \subset C, C \subset K
           & D / B \subset 'Z(C / B)]%g ->
   (*b*) coherent (S A) L^# tau -> \unless coherent (S B) L^# tau,
-  #|K : A|%:R - 1 <= 2%:R * #|L : C|%:R * sqrtC #|C : D|%:R :> algC.
+  #|K : A|%:R - 1 <= 2 * #|L : C|%:R * sqrtC #|C : D|%:R :> algC.
 Proof.
 move=> [nsAL nsBL nsCL nsDL] [ltAK sBD sDC sCK sDbZC] cohA.
 have sBC := subset_trans sBD sDC; have sBK := subset_trans sBC sCK.
@@ -152,7 +152,7 @@ have ltAH: A \proper H.
   by rewrite properEneq sAH (contraTneq _ lbHA) // => ->; rewrite indexgg addn1.
 set x : algC := sqrtC #|H : A|%:R.
 have [nz_x x_gt0]: x != 0 /\ 0 < x by rewrite gt_eqF sqrtC_gt0 gt0CiG.
-without loss{cohA} ubKA: / #|K : A|%:R - 1 <= 2%:R * #|L : H|%:R * x.
+without loss{cohA} ubKA: / #|K : A|%:R - 1 <= 2 * #|L : H|%:R * x.
   have [sAK ltAK] := (subset_trans sAH sHK, proper_sub_trans ltAH sHK).
   exact: coherent_seqIndD_bound id.
 suffices{lbHA}: (x - x^-1) ^+ 2 <= (2 * #|L : K|)%:R ^+ 2.
@@ -713,7 +713,7 @@ have oYtau: orthonormal (map tau1 Y) by apply: map_orthonormal.
 have [[_ oYY] [_ oYYt]] := (orthonormalP oY, orthonormalP oYtau).
 have [eta1 Yeta1]: {eta1 | eta1 \in Y} by apply: seqIndD_nonempty.
 pose m : algC := (size Y)%:R; pose m_ub2 a := (a - 1) ^+ 2 + (m - 1) * a ^+ 2.
-have m_ub2_lt2 a: a \in Num.int -> m_ub2 a < 2%:R ->
+have m_ub2_lt2 a: a \in Num.int -> m_ub2 a < 2 ->
                   a = 0 \/ a = 1 /\ size Y = 2%N.
   move=> Za ub_a; have [|nza] := eqVneq a 0; [by left | right].
   have ntY: (1 < size Y)%N by apply: seqInd_nontrivial Yeta1.
@@ -873,7 +873,7 @@ have{odd_frobL1} caseA_cohXY: caseA -> coherent (X ++ Y) L^# tau.
     rewrite addrC cfnormB !cfnormZ intr_normK ?norm_natr // cfdotZr.
     rewrite cfnorm_map_orthonormal // -/m linear_sum cfproj_sum_orthonormal //.
     by rewrite oYYt ?map_f // eqxx mulr1 rmorphM/= conjCK aut_natr ?aut_intr.
-  have{norm_tau_psi1} mq2_lt2: m_ub2 q < 2%:R.
+  have{norm_tau_psi1} mq2_lt2: m_ub2 q < 2.
     suffices a2_gt1: a ^+ 2 > 1.
       have /ltr_pM2l <-: a ^+ 2 > 0 by apply: lt_trans a2_gt1.
       rewrite -(ltrD2l '[X1]) -norm_tau_psi1 ltr_wpDl ?cfnorm_ge0 //.
@@ -1057,8 +1057,8 @@ have{caseA_cohXY Itau1 Ztau1 Dtau1 oYYt} cohXY: coherent (X ++ Y) L^# tau.
       rewrite -oW1 (card_isog (quotient_isog nZW1 tiZW1)) -card_quotient //.
       rewrite dvdn_leq ?(Frobenius_dvd_ker1 frobL2) // -subn1 subn_gt0.
       by rewrite cardG_gt1; case/Frobenius_context: frobL2.
-    have{ub_norm_gamma} ub_xm: m_ub2 x < 2%:R.
-      have: '[Y1] < 2%:R.
+    have{ub_norm_gamma} ub_xm: m_ub2 x < 2.
+      have: '[Y1] < 2.
         rewrite -2!(ltr_pM2l (gt0CiG H Z)) -!natrM mulnA muln2.
         apply: le_lt_trans ub_norm_gamma; rewrite Dgamma cfnormBd.
           by rewrite cfnormZ normCK rmorph_nat mulrA -subr_ge0 addrK cfnorm_ge0.
diff --git a/theories/PFsection7.v b/theories/PFsection7.v
index 5d1b99c..ffa40bc 100644
--- a/theories/PFsection7.v
+++ b/theories/PFsection7.v
@@ -351,7 +351,7 @@ Lemma Dade_Ind1_sub_lin (nu : {additive 'CF(L) -> 'CF(G)}) zeta :
       (*a2*) [/\ orthogonal calSnu Gamma, '[Gamma, 1] = 0
              & exists2 a, a \in Num.int
              & beta = 1 - nu zeta + a *: sumSnu + Gamma]
-    & (*b*) e <= (h - 1) / 2%:R ->
+    & (*b*) e <= (h - 1) / 2 ->
             '[(nu zeta)^\rho] >= 1 - e / h /\ '[Gamma] <= e - 1
     & (*c*) {in irr G, forall chi : 'CF(G), orthogonal calSnu chi ->
         [/\ {in A, forall x, chi^\rho x = '[beta, chi]}
@@ -477,7 +477,7 @@ split=> // [ | chi /irrP[t def_chi] o_chiSnu].
     by rewrite -mulrN -sqrrN addr_ge0 ?(u_ge0, mulr_ge0) ?oppr_ge0 ?ler0n.
   rewrite -real_ltNge ?Rreal_int // lt_def => /andP[].
   move/(norm_intr_ge1 Za)=> a_ge1 a_ge0; rewrite mulrA -mulrBl.
-  rewrite (normr_idP _) // -(@mulVf _ 2%:R) ?pnatr_eq0 // in a_ge1.
+  rewrite (normr_idP _) // -(@mulVf _ 2) ?pnatr_eq0 // in a_ge1.
   rewrite mulr_ge0 // subr_ge0 (le_trans _ (ler_wpM2l u_ge0 a_ge1)) // mulrA.
   by rewrite ler_wpM2r ?ler0n // -(ler_pM2l L_gt0) mulrA Lu -eh mulfK.
 have Zchi: chi \in 'Z[irr G] by rewrite def_chi irr_vchar.
@@ -614,7 +614,7 @@ End DisjointDadeOrtho.
 (* A numerical fact used in Sections 7 and 14. *)
 Lemma odd_Frobenius_index_ler (R : numFieldType) (K L : {group gT}) :
     odd #|L| -> [Frobenius L with kernel K] ->
-  #|L : K|%:R <= (#|K|%:R - 1) / 2%:R :> R.
+  #|L : K|%:R <= (#|K|%:R - 1) / 2 :> R.
 Proof.
 move=> oddL /existsP[H frobL]; rewrite ler_pdivlMr ?ltr0n // lerBrDl.
 have ->: #|L : K| = #|H| by have [/index_sdprod] := Frobenius_context frobL.
@@ -644,7 +644,7 @@ Hypothesis k_ge2: (k >= 2)%N.
 (*c*) Hypothesis card_coprime : forall i j, i != j -> coprime #|H i| #|H j|.
 
 (* A numerical fact that is used in both (7.10) and (7.11) *)
-Let e_bounds i : 1 < e_ i /\ e_ i <= (h_ i - 1) / 2%:R.
+Let e_bounds i : 1 < e_ i /\ e_ i <= (h_ i - 1) / 2.
 Proof.
 have [/oddSg/(_ oddG)oddL _ frobL] := frobeniusL_G i.
 rewrite ltr1n odd_Frobenius_index_ler ?(FrobeniusWker frobL) //.
@@ -653,7 +653,7 @@ Qed.
 
 (* This is Peterfalvi (7.10). *)
 Lemma coherent_Frobenius_bound : exists i, let e := e_ i in let h := h_ i in
-  (e - 1) * ((h - 2%:R * e - 1) / (e * h) + 2%:R / (h * (h + 2%:R)))
+  (e - 1) * ((h - 2 * e - 1) / (e * h) + 2 / (h * (h + 2)))
      <= (#|G0|%:R - 1) / #|G|%:R.
 Proof.
 have [sLG solL frobL] := all_and3 frobeniusL_G.
@@ -708,7 +708,7 @@ have h_gt1 i: 1 < h_ i by rewrite ltr1n cardG_gt1.
 have eh i: e_ i * h_ i = #|L i|%:R by rewrite -natrM mulnC Lagrange.
 have def_h1 i: h_ i - 1 = #|A i|%:R.
   by rewrite /h_ (cardsD1 1%g) group1 addnC natrD addrK.
-have [i1 min_i1]: {i1 | forall i, i != i1 -> h_ i1 + 2%:R <= h_ i}.
+have [i1 min_i1]: {i1 | forall i, i != i1 -> h_ i1 + 2 <= h_ i}.
   exists [arg min_(i < Ordinal k_ge2) #|H i|].
   case: fintype.arg_minnP => // i1 _ min_i1.
   have oddH i: #|H i| = #|H i|./2.*2.+1.
@@ -718,9 +718,9 @@ have [i1 min_i1]: {i1 | forall i, i != i1 -> h_ i1 + 2%:R <= h_ i}.
   apply: contraTneq (card_coprime neq_i) => eqHii1.
   by rewrite oddH -eqHii1 -oddH /coprime gcdnn -trivg_card1.
 exists i1 => e h; set lhs := (e - 1) * _.
-have nzh2: h + 2%:R != 0 by rewrite -natrD addnC pnatr_eq0.
-have{lhs} ->: lhs = 1 - e / h - (h - 1) / (e * h) - (e - 1) / (h + 2%:R).
-  rewrite {}/lhs -{2}(addrK h 2%:R) !invfM (mulrBl _ _ h) mulVKf ?nzh //.
+have nzh2: h + 2 != 0 by rewrite -natrD addnC pnatr_eq0.
+have{lhs} ->: lhs = 1 - e / h - (h - 1) / (e * h) - (e - 1) / (h + 2).
+  rewrite {}/lhs -{2}(addrK h 2) !invfM (mulrBl _ _ h) mulVKf ?nzh //.
   rewrite addrCA (addrC _ h) mulrCA mulrA addrA mulrBr; congr (_ - _).
   rewrite mulfK // mulrDr addrAC [LHS]addrC mulrC mulrBl -mulrA mulVKf ?nze //.
   rewrite mulrC mulrBr mulrBl mul1r [X in X + _]addrAC addrC addrA.
@@ -736,7 +736,7 @@ have [_ lt_e_h2] := e_bounds i1; rewrite -/(rho _) -/(h_ _) -/h.
 case/(_ lt_e_h2)=> min_rho1 maxGamma _ {lt_e_h2}.
 pose calB := [set i | (i != i1) && (c i i1 == 0)].
 pose sumB := \sum_(i in calB) (h_ i - 1) / (e_ i * h_ i).
-suffices{min_rho1} sumB_max: sumB <= (e - 1) / (h + 2%:R).
+suffices{min_rho1} sumB_max: sumB <= (e - 1) / (h + 2).
   rewrite -subr_ge0 opprB addrCA -[_ / _ - _]opprB subr_ge0.
   apply: le_trans sumB_max.
   rewrite -subr_ge0 opprB addrCA -(opprB _ sumB) subr_ge0.
@@ -824,7 +824,7 @@ have [i] := coherent_Frobenius_bound; apply: contraTneq => ->.
 have [] := e_bounds i; set e := e_ i; set h := h_ i => e_gt1 le_e_h2.
 rewrite cards1 subrr mul0r lt_geF // pmulr_rgt0 ?subr_gt0 // ltr_wpDl //.
   rewrite ?(mulr_ge0, invr_ge0) ?ler0n // addrAC subr_ge0.
-  by rewrite -[_ - 1](@divfK _ 2%:R) ?pnatr_eq0 // mulrC ler_wpM2r ?ler0n.
+  by rewrite -[_ - 1](@divfK _ 2) ?pnatr_eq0 // mulrC ler_wpM2r ?ler0n.
 by rewrite -natrD addnC ?(pmulr_rgt0, invr_gt0) ?ltr0n.
 Qed.