diff --git a/refinements/karatsuba.v b/refinements/karatsuba.v
index f29e0b4..5c147e7 100644
--- a/refinements/karatsuba.v
+++ b/refinements/karatsuba.v
@@ -76,8 +76,8 @@ rewrite [p in RHS](rdivp_eq (monicXn _ m)) [q in RHS](rdivp_eq (monicXn _ m)).
 rewrite /shift_op /shift_polyR /shiftp /implem /implem_nat /implem_id.
 simpC.
 rewrite !ih !(mulrDl, mulrDr, mulNr) mulnC exprM.
-rewrite -addrA -addrA -opprD [X in X + _ - _]addrC [in LHS]addrACA addrK.
-by rewrite !(commr_polyXn, mulrA, addrA).
+rewrite -[in X in X + _]addrA -opprD [X in X + _ - _]addrC [in LHS]addrACA.
+by rewrite addrK !(commr_polyXn, mulrA, addrA).
 Qed.
 
 Lemma karatsubaE (p q : {poly R}) : karatsuba (N:=nat) p q = p * q.
diff --git a/theory/dvdring.v b/theory/dvdring.v
index a9507f7..6ef0acf 100644
--- a/theory/dvdring.v
+++ b/theory/dvdring.v
@@ -1792,8 +1792,8 @@ HB.builders Context R of IntegralDomain_isEuclidean R.
   rewrite (eqd_trans (gcdrE _ _)) ?(eqd_trans (ihn' _ _)) //;
     do ?by rewrite -ltnS (leq_trans (mod_spec _ _)) ?b0 //.
   rewrite mulrBl addrA [v * a + _]addrC -mulrA -addrA -mulrBr /div b0.
-  case: edivP ihn'=> /= q r.
-  move/eqP; rewrite addrC -subr_eq; move/eqP=>->.
+  case: edivP ihn'=> /= q r /eqP.
+  rewrite [_ + r]addrC -subr_eq; move/eqP=>->.
   by rewrite b0 /= => nrb; apply; rewrite -ltnS (leq_trans nrb).
   Qed.