diff --git a/theories/abel.v b/theories/abel.v
index 6d277f5..6c35a53 100644
--- a/theories/abel.v
+++ b/theories/abel.v
@@ -1226,7 +1226,7 @@ Proof.
 rewrite separable_poly.unlock.
 apply/coprimepP => q /(irredp_XsubCP irreducible_example) [//| eqq].
 have size_deriv_example : size poly_example^`() = 5%N.
-  rewrite !derivCE addr0 alg_polyC -scaler_nat addr0.
+  rewrite !derivCE ?mul0rn ?addr0 alg_polyC -scaler_nat.
   by rewrite size_addl ?size_scale ?size_opp ?size_polyXn ?size_polyC.
 rewrite gtNdvdp -?size_poly_eq0 ?size_deriv_example//.
 by rewrite (eqp_size eqq) ?size_poly_example.
@@ -1263,7 +1263,7 @@ by rewrite separable_map separable_example.
 Qed.
 
 Lemma deriv_poly_example : poly_example^`() = 5%:R *: 'X^4 - 4%:R%:P.
-Proof. by rewrite /poly_example !derivE addr0 alg_polyC scaler_nat ?addr0. Qed.
+Proof. by rewrite /poly_example !derivE ?mul0rn?addr0 alg_polyC scaler_nat. Qed.
 
 Lemma deriv_poly_example_neq0 : poly_example^`() != 0.
 Proof.
diff --git a/theories/xmathcomp/map_gal.v b/theories/xmathcomp/map_gal.v
index cddf7b5..29d86c4 100644
--- a/theories/xmathcomp/map_gal.v
+++ b/theories/xmathcomp/map_gal.v
@@ -556,7 +556,7 @@ Qed.
 Lemma gal_kAEndf (K E : {subfield L}) : (K <= E)%VS ->
    (gal E @* kAEndf K)%g = (gal E @* kAEnd K E)%g :> {set _}.
 Proof.
-move=> KE; rewrite kAEnd_split morphimIG ?ker_gal ?kAEndSl// (setIidPr _)//=.
+move=> KE; rewrite (kAEnd_split K) morphimIG ?ker_gal ?kAEndSl ?(setIidPr _)//=.
 by rewrite (subset_trans (morphim_sub _ _))//= morphimS// subfield_closed.
 Qed.
 
diff --git a/theories/xmathcomp/various.v b/theories/xmathcomp/various.v
index 3047c2c..2aa5b9c 100644
--- a/theories/xmathcomp/various.v
+++ b/theories/xmathcomp/various.v
@@ -1100,7 +1100,7 @@ have phixy : phi (tperm x y) = tperm 0 k.
   apply/permP => i; rewrite permE/= /gsf/=; apply: (canLR fK).
   by rewrite !permE/= -f0 -[y]gK !(can_eq fK) -!fun_if.
 have phic : phi c = perm (addrI 1%R).
-  apply/permP => i; rewrite permE /gsf/=; apply: (canLR fK).
+  apply/permP => i; rewrite [LHS]permE /gsf/=; apply: (canLR fK).
   by rewrite !permE /f /Zpm -permM addrC expgDzmod.
 rewrite -(injmSK phi_inj)//= morphim_gen/= ?subsetT//= -/phi.
 rewrite phiT /morphim !setTI/= -/phi imsetU1 imset_set1/= phixy phic.