diff --git a/theories/PFsection10.v b/theories/PFsection10.v
index 1f3f7f4..34c76bc 100644
--- a/theories/PFsection10.v
+++ b/theories/PFsection10.v
@@ -539,7 +539,7 @@ have odd_zeta_g: (zeta^\tau1 g == 1 %[mod 2])%C.
   pose eW1 := [pred i : Iirr W1 | conjC_Iirr i < i]%N.
   rewrite (bigID eW1) (reindex_inj (can_inj (@conjC_IirrK _ _))) /=.
   set s1 := \sum_(i | _) _; set s2 := \sum_(i | _) _; suffices ->: s1 = s2.
-    by rewrite -mulr2n addrC -(mulr_natr _ 2) eqCmod_addl_mul ?rpred_sum.
+    by rewrite -mulr2n addrC -[X in X + 1]mulr_natr eqCmod_addl_mul ?rpred_sum.
   apply/eq_big=> [i | i _].
     rewrite (canF_eq (@conjC_IirrK _ _)) conjC_Iirr0 conjC_IirrK -leqNgt.
     rewrite ltn_neqAle val_eqE -irr_eq1 (eq_sym i) -(inj_eq irr_inj) andbA.
diff --git a/theories/PFsection7.v b/theories/PFsection7.v
index e34dbb9..d050963 100644
--- a/theories/PFsection7.v
+++ b/theories/PFsection7.v
@@ -515,7 +515,7 @@ Proof.
 move=> [Zphi Rphi] [Zpsi Rpsi]; rewrite cfdot_vchar_r // (bigD1 (0 : 'I__)) //=.
 rewrite addrC -irr0 (bigID [pred i | conjC_Iirr i < i]%N) /=.
 set a1 := \sum_(i | _) _; set a2 := \sum_(i | _) _; suffices ->: a1 = a2.
-  rewrite -mulr2n -mulr_natr (rpredDl _ (dvdC_mull _ _)) //; last first.
+  rewrite -mulr2n -[_ *+ 2]mulr_natr (rpredDl _ (dvdC_mull _ _)) //; last first.
     by rewrite rpred_sum // => i; rewrite rpredM ?Cint_cfdot_vchar_irr.
   have /CintP[m1 ->] := Cint_cfdot_vchar_irr 0 Zphi.
   have /CintP[m2 ->] := Cint_cfdot_vchar_irr 0 Zpsi.