diff --git a/classical/mathcomp_extra.v b/classical/mathcomp_extra.v
index 77ec6d0316..c5842dca81 100644
--- a/classical/mathcomp_extra.v
+++ b/classical/mathcomp_extra.v
@@ -245,7 +245,7 @@ Proof. by move=> F0; elim/big_rec : _ => // i x Pi; apply/ler_wnDl/F0. Qed.
 Inductive boxed T := Box of T.
 
 Reserved Notation "`1- r" (format "`1- r", at level 2).
-Reserved Notation "f \^-1" (at level 3, format "f \^-1", left associativity).
+Reserved Notation "f \^-1" (at level 35, format "f \^-1").
 
 (* TODO: To be backported to finmap *)
 
diff --git a/theories/altreals/realseq.v b/theories/altreals/realseq.v
index 842e6a9104..7ffeb6136b 100644
--- a/theories/altreals/realseq.v
+++ b/theories/altreals/realseq.v
@@ -213,7 +213,7 @@ apply/asboolP/nboundedP; exists e => [|n]; first by rewrite lt_max ltr_wpDl.
 case: (ltnP n K); last first.
   move/cu; rewrite inE eclamp_id ?ltr01 // => ltunBx1.
   rewrite lt_max; apply/orP; left; rewrite -[u n](addrK x) addrAC.
-  by apply/(le_lt_trans (ler_normD _ _)); rewrite addrC ltrD2l.
+  by apply/(le_lt_trans (ler_normD _ _)); rewrite [ltLHS]addrC ltrD2l.
 move=> lt_nK; have: `|u n| \in S; first by apply/map_f; rewrite mem_iota.
 move=> un_S; rewrite lt_max; apply/orP; right.
 case E: {+}K lt_nK => [|k] // lt_nSk; apply/ltr_pwDr; first apply/ltr01.
diff --git a/theories/derive.v b/theories/derive.v
index 312b964874..95a059ab40 100644
--- a/theories/derive.v
+++ b/theories/derive.v
@@ -721,7 +721,7 @@ Fact dcomp (U V' W' : normedModType R) (f : U -> V') (g : V' -> W') x :
 Proof.
 move=> df dg; split; first by move=> ?; apply: continuous_comp.
 apply: eqaddoEx => y; rewrite diff_locallyx// -addrA diff_locallyxC// linearD.
-rewrite addrA -addrA; congr (_ + _ + _).
+rewrite addrA -[LHS]addrA; congr (_ + _ + _).
 rewrite diff_eqO // ['d f x : _ -> _]diff_eqO //.
 by rewrite {2}eqoO addOx compOo_eqox compoO_eqox addox.
 Qed.
diff --git a/theories/esum.v b/theories/esum.v
index 9df507fb1d..b4b6e07a44 100644
--- a/theories/esum.v
+++ b/theories/esum.v
@@ -273,7 +273,7 @@ apply lee_fsum=> [|i Xi]; first exact: finite_set_fst.
 rewrite ereal_sup_ubound //=; have ? : finite_set (X.`2 `&` J i).
   by apply: finite_setI; left; exact: finite_set_snd.
 exists (X.`2 `&` J i) => //.
-rewrite [in RHS]big_fset_condE/= fsbig_finite//; apply eq_fbigl => j.
+rewrite [in RHS]big_fset_condE/= fsbig_finite//; apply/eq_fbigl => j.
 by rewrite in_fset_set// !inE/= in_setI in_fset_set//; exact: finite_set_snd.
 Qed.
 
diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v
index 7bf196baca..c17f5ba829 100644
--- a/theories/lebesgue_integral.v
+++ b/theories/lebesgue_integral.v
@@ -5902,7 +5902,7 @@ move: a0; rewrite le_eqVlt => /predU1P[a0|a0].
   move=> y; rewrite /ball/= => xyd.
   have ? : ball x r `<=` ball y (r + d).
     move=> /= z; rewrite /ball/= => xzr; rewrite -(subrK x y) -(addrA (y - x)%R).
-    by rewrite (le_lt_trans (ler_normD _ _))// addrC ltrD// distrC.
+    by rewrite (le_lt_trans (ler_normD _ _))// [ltLHS]addrC ltrD// distrC.
   have ? : k <= \int[mu]_(y in ball y (r + d)) `|(f y)%:E|.
     apply: ge0_subset_integral =>//; [exact:measurable_ball|
                                       exact:measurable_ball|].
@@ -5940,7 +5940,7 @@ exists (ball x d).
 move=> y; rewrite /ball/= => xyd.
 have ? : ball x r `<=` ball y (r + d).
   move=> /= z; rewrite /ball/= => xzr; rewrite -(subrK x y) -(addrA (y - x)%R).
-  by rewrite (le_lt_trans (ler_normD _ _))// addrC ltrD// distrC.
+  by rewrite (le_lt_trans (ler_normD _ _))// [ltLHS]addrC ltrD// distrC.
 have ? : k <= \int[mu]_(z in ball y (r + d)) `|(f z)%:E|.
   apply: ge0_subset_integral => //; [exact: measurable_ball|
                                      exact: measurable_ball|].
diff --git a/theories/topology.v b/theories/topology.v
index eb7c846cb6..95ceb7f9fd 100644
--- a/theories/topology.v
+++ b/theories/topology.v
@@ -5824,7 +5824,7 @@ move: e1 e2 x z; elim: n.
     - apply: n_step_ball_le; last exact: Oxy.
       by rewrite -deE lerDl; apply: ltW.
     - apply: (@n_step_ball_le _ _ d2); last by split.
-      rewrite -[e2]addr0 -(subrr e1) addrA -lerBlDr opprK addrC.
+      rewrite -[e2]addr0 -(subrr e1) addrA -lerBlDr opprK [leLHS]addrC.
       by rewrite [e2 + _]addrC -deE; exact: lerD.
     - by rewrite addn0.
   move=> /negP; rewrite -ltNge//.