diff --git a/classical/mathcomp_extra.v b/classical/mathcomp_extra.v
index f0ecf3733..f2c287308 100644
--- a/classical/mathcomp_extra.v
+++ b/classical/mathcomp_extra.v
@@ -156,14 +156,14 @@ Lemma maxr_absE (x y : R) : Num.max x y = (x + y + `|x - y|) / 2%:R.
 Proof.
 apply: canRL (mulfK _) _ => //; rewrite ?pnatr_eq0//.
 case: lerP => _; (* TODO: ring *) rewrite [2%:R]mulr2n mulrDr mulr1.
-  by rewrite addrACA subrr addr0.
+  by rewrite addrCA addrK.
 by rewrite addrCA addrAC subrr add0r.
 Qed.
 
 Lemma minr_absE (x y : R) : Num.min x y = (x + y - `|x - y|) / 2%:R.
 Proof.
 apply: (addrI (Num.max x y)); rewrite addr_max_min maxr_absE. (* TODO: ring *)
-by rewrite -mulrDl addrACA subrr addr0 mulrDl -splitr.
+by rewrite -mulrDl addrCA addrK mulrDl -splitr.
 Qed.
 
 End max_min.
@@ -304,8 +304,7 @@ Lemma onem0 : `1-0 = 1. Proof. by rewrite /onem subr0. Qed.
 
 Lemma onem1 : `1-1 = 0. Proof. by rewrite /onem subrr. Qed.
 
-Lemma onemK r : `1-(`1-r) = r.
-Proof. by rewrite /onem opprB addrCA subrr addr0. Qed.
+Lemma onemK r : `1-(`1-r) = r. Proof. exact: subKr. Qed.
 
 Lemma add_onemK r : r + `1- r = 1.
 Proof. by rewrite /onem addrC subrK. Qed.
diff --git a/classical/set_interval.v b/classical/set_interval.v
index b3714b83d..6f18fa46c 100644
--- a/classical/set_interval.v
+++ b/classical/set_interval.v
@@ -540,7 +540,7 @@ Lemma line_path1 a b : line_path a b 1 = b.
 Proof. by rewrite /line_path subrr mul0r add0r mul1r. Qed.
 
 Lemma line_path_sym a b t : line_path a b t = line_path b a (1 - t).
-Proof. by rewrite /line_path opprB addrCA subrr addr0 addrC. Qed.
+Proof. by rewrite /line_path subKr addrC. Qed.
 
 Lemma line_path_flat a : line_path a a = cst a.
 Proof. by apply/funext => t; rewrite line_pathEl subrr mulr0 add0r. Qed.
diff --git a/reals/itv.v b/reals/itv.v
index 3a4b37465..7ac9e597b 100644
--- a/reals/itv.v
+++ b/reals/itv.v
@@ -888,10 +888,7 @@ Definition s_of_pq (p q : {i01 R}) : {i01 R} :=
   (1 - ((1 - p%:inum)%:i01%:inum * (1 - q%:inum)%:i01%:inum))%:i01.
 
 Lemma s_of_p0 (p : {i01 R}) : s_of_pq p 0%:i01 = p.
-Proof.
-apply/val_inj => /=.
-by rewrite subr0 mulr1 opprB addrCA subrr addr0.
-Qed.
+Proof. by apply/val_inj; rewrite /= subr0 mulr1 subKr. Qed.
 
 Canonical onem_itv01 (p : {i01 R}) : {i01 R} :=
   @Itv.mk _ _ (onem p%:inum) [itv of 1 - p%:inum].
diff --git a/reals/reals.v b/reals/reals.v
index 5e0503ca1..bc9d85ce1 100644
--- a/reals/reals.v
+++ b/reals/reals.v
@@ -81,8 +81,7 @@ Proof. by rewrite predeqE => r; split => // _. Qed.
 Lemma lboundT : lbound [set: R] = set0.
 Proof.
 rewrite predeqE => r; split => // /(_ (r - 1) Logic.I).
-rewrite lerBrDl addrC -lerBrDl subrr.
-by rewrite real_leNgt ?realE ?ler01// ?lexx// ltr01.
+by rewrite addrC -subr_ge0 addrK ler0N1.
 Qed.
 
 End subr_image.
@@ -277,8 +276,7 @@ Proof.
 move=> has_supE; rewrite orC.
 case: (lerP (sup E) x)=> hx /=; [by left|right].
 have /sup_adherent/(_  has_supE) : 0 < sup E - x by rewrite subr_gt0.
-case=> e Ee hlte; apply/downP; exists e => //; move: hlte.
-by rewrite opprB addrCA subrr addr0 => /ltW.
+by case=> e Ee; rewrite subKr => /ltW hlte; apply/downP; exists e.
 Qed.
 
 Lemma sup_le_ub {E} x : E !=set0 -> (ubound E) x -> sup E <= x.
@@ -452,7 +450,7 @@ rewrite le_eqVlt=> /orP[/eqP<-//| lt_yFx].
 rewrite ltrBlDr -ltrBlDl => lt1_FxBy.
 pose e := sup (floor_set x) - y; have := has_sup_floor_set x.
 move/sup_adherent=> -/(_ e) []; first by rewrite subr_gt0.
-move=> z Fz; rewrite /e opprB addrCA subrr addr0 => lt_yz.
+move=> z Fz; rewrite /= subKr => lt_yz.
 have /sup_upper_bound /ubP /(_ _ Fz) := has_sup_floor_set x.
 rewrite -(lerD2r (-y)) => /le_lt_trans /(_ lt1_FxBy).
 case/andP: Fy Fz lt_yz=> /RintP[yi -> _].
@@ -644,7 +642,7 @@ Lemma lt_inf_imfset {T : Type} (F : T -> R) l :
   exists2 x, F x < l & inf [set y | exists x, y = F x] <= F x.
 Proof.
 set P := [set y | _]; move=> hs; rewrite -subr_gt0.
-move=> /inf_adherent/(_ hs)[_ [x ->]]; rewrite addrCA subrr addr0 => ltFxl.
+move=> /inf_adherent/(_ hs)[_ [x ->]]; rewrite addrC subrK => ltFxl.
 by exists x => //; rewrite (inf_lbound hs.2)//; exists x.
 Qed.
 
diff --git a/theories/derive.v b/theories/derive.v
index da703d8d1..fc68330d6 100644
--- a/theories/derive.v
+++ b/theories/derive.v
@@ -254,7 +254,7 @@ Proof.
 move=> df; apply/eqaddoP => _/posnumP[e].
 rewrite -nbhs_nearE nbhs_simpl /= dnbhsE; split; last first.
   rewrite /at_point opprD -![(_ + _ : _ -> _) _]/(_ + _) scale0r add0r.
-  by rewrite addrA subrr add0r normrN scale0r !normr0 mulr0.
+  by rewrite addrCA addKr normrN scale0r !normr0 mulr0.
 have /eqolimP := df.
 move=> /eqaddoP /(_ e%:num) /(_ [gt0 of e%:num]).
 apply: filter_app; rewrite /= !near_simpl near_withinE; near=> h => hN0.
@@ -973,7 +973,7 @@ rewrite normrN [leRHS]ger0_norm; last first.
   rewrite subr_ge0; apply: ltW; apply: lt_le_trans lthhx _.
   by rewrite ler_pdivrMr // -{1}(mulr1 `|x|) ler_pM // ler1n.
 rewrite lerBrDr -lerBrDl (splitr `|x|).
-by rewrite normrM normfV (@ger0_norm _ 2) // -addrA subrr addr0; apply: ltW.
+by rewrite normrM normfV (@ger0_norm _ 2) // addrK; apply/ltW.
 Unshelve. all: by end_near. Qed.
 
 Lemma diff_Rinv (x : R) : x != 0 ->
@@ -1569,15 +1569,14 @@ Proof.
 move=> altb fdrvbl fcont.
 set g := f + (- ( *:%R^~ ((f b - f a) / (b - a)) : R -> R)).
 have gdrvbl x : x \in `]a, b[%R -> derivable g x 1.
-  by move=> /fdrvbl dfx; apply: derivableB => //; exact/derivable1_diffP.
+  by move=> /fdrvbl dfx; apply/derivableB/derivable1_diffP.
 have gcont : {within `[a, b], continuous g}.
-  move=> x; apply: continuousD _ ; first by move=>?; exact: fcont.
-  by apply/continuousN/continuous_subspaceT=> ?; exact: scalel_continuous.
+  move=> x; apply: continuousD _ ; first exact: fcont.
+  exact/continuousN/continuous_subspaceT/scalel_continuous.
 have gaegb : g a = g b.
   rewrite /g -![(_ - _ : _ -> _) _]/(_ - _).
   apply/eqP; rewrite -subr_eq /= opprK addrAC -addrA -scalerBl.
-  rewrite [_ *: _]mulrA mulrC mulrA mulVf.
-    by rewrite mul1r addrCA subrr addr0.
+  rewrite [_ *: _]mulrC divfK; first by rewrite addrC subrK.
   by apply: lt0r_neq0; rewrite subr_gt0.
 have [c cab dgc0] := Rolle altb gdrvbl gcont gaegb.
 exists c; first exact: cab.
diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v
index 5b2df0336..c9b2bbfaf 100644
--- a/theories/lebesgue_integral.v
+++ b/theories/lebesgue_integral.v
@@ -348,8 +348,8 @@ Lemma sfun_rect (K : T -> Type) :
   (forall f (Pf : f \in sfun), K (sfun_Sub Pf)) -> forall u : T, K u.
 Proof.
 move=> Ksub [f [[Pf1] [Pf2]]]; have Pf : f \in sfun by apply/andP; rewrite ?inE.
-have -> : Pf1 = (set_mem (sub_sfun_mfun Pf)) by [].
-have -> : Pf2 = (set_mem (sub_sfun_fimfun Pf)) by [].
+have -> : Pf1 = set_mem (sub_sfun_mfun Pf) by [].
+have -> : Pf2 = set_mem (sub_sfun_fimfun Pf) by [].
 exact: Ksub.
 Qed.
 
@@ -451,24 +451,18 @@ Qed.
 Lemma preimage_cstM T (R : realFieldType) (x y : R) (f : T -> R) :
   x != 0 -> (cst x \* f) @^-1` [set y] = f @^-1` [set y / x].
 Proof.
-move=> x0; apply/seteqP; rewrite /preimage; split => [z/= <-|z/= ->].
-  by rewrite mulrAC divrr ?mul1r// unitfE.
-by rewrite mulrCA divrr ?mulr1// unitfE.
+move=> x0; apply/seteqP.
+by split=> [z/= <-|z/= ->]; rewrite [x * _]mulrC (mulfK, divfK).
 Qed.
 
 Lemma preimage_add T (R : numDomainType) (f g : T -> R) z :
   (f \+ g) @^-1` [set z] = \bigcup_(a in f @` setT)
     ((f @^-1` [set a]) `&` (g @^-1` [set z - a])).
 Proof.
-apply/seteqP; split=> [x /= fgz|x [_ /= [y _ <-]] []].
-  have : z - f x \in g @` setT.
-    by rewrite inE /=; exists x=> //; rewrite -fgz addrC addKr.
-  rewrite inE /= => -[x' _ gzf]; exists (z - g x')%R => /=.
-    by exists x => //; rewrite gzf opprB addrC subrK.
-  rewrite /preimage /=; split; first by rewrite gzf opprB addrC subrK.
-  by rewrite gzf opprB addrC subrK -fgz addrC addKr.
-rewrite /preimage /= => [fxfy gzf].
-by rewrite gzf -fxfy addrC subrK.
+apply/seteqP; split=> [x /= fgz|x [_ /= [y _ <-]] [fxfy gzf]]; last first.
+  by rewrite gzf -fxfy addrC subrK.
+exists (z - g x); first by exists x; rewrite // -fgz addrK.
+by split; rewrite 1?subKr // -fgz addrK.
 Qed.
 
 Section simple_bounded.
@@ -483,6 +477,7 @@ exists (fine (\big[maxe/-oo%E]_(i <- r) `|i|%:E)).
 split; rewrite ?num_real// => x mx z _; apply/ltW/(le_lt_trans _ mx).
 have ? : f z \in r by have := imageT f z; rewrite fr.
 rewrite -[leLHS]/(fine `|f z|%:E) fine_le//.
+  (* TODO: generalize the statement of bigmaxe_fin_num *)
   have := @bigmaxe_fin_num _ (map normr r) `|f z|.
   by rewrite big_map => ->//; apply/mapP; exists (f z).
 by rewrite (bigmax_sup_seq _ _ (lexx _)).
@@ -586,14 +581,14 @@ Import HBNNSimple.
 Lemma nnsfun_cover : \big[setU/set0]_(i \in range f) (f @^-1` [set i]) = setT.
 Proof. by rewrite fsbig_setU//= -subTset => x _; exists (f x). Qed.
 
-Lemma nnsfun_coverT :
-  \big[setU/set0]_(i \in [set: R]) (f @^-1` [set i]) = setT.
+Lemma nnsfun_coverT : \big[setU/set0]_(i \in [set: R]) f @^-1` [set i] = setT.
 Proof.
-by rewrite -(fsbig_widen (range f)) ?nnsfun_cover//= => x [_ /= /preimage10->].
+by rewrite -(fsbig_widen (range f)) ?nnsfun_cover//= => x [_ /preimage10].
 Qed.
 
 End nnsfun_cover.
 
+(* FIXME: shouldn't we avoid calling [done] in a hint? *)
 #[global] Hint Extern 0 (measurable (_ @^-1` [set _])) =>
   solve [apply: measurable_sfunP; exact: measurable_set1] : core.
 
@@ -626,8 +621,8 @@ Lemma additive_nnsfunr (g f : {nnsfun T >-> R}) x :
   m (f @^-1` [set x] `&` \big[setU/set0]_(i \in range g) (g @^-1` [set i])).
 Proof.
 rewrite -?measure_fsbig//.
-- by rewrite !fsbig_finite//= big_distrr//.
-- by move=> i Ai; apply: measurableI => //.
+- by rewrite !fsbig_finite//= big_distrr.
+- by move=> i Ai; apply: measurableI.
 - exact/trivIset_setIl/trivIset_preimage1.
 Qed.
 
@@ -644,8 +639,8 @@ Local Open Scope ereal_scope.
 Let mulef_ge0 (R : realDomainType) x (f : R -> \bar R) :
   0 <= f x -> ((x < 0)%R -> f x = 0) -> 0 <= x%:E * f x.
 Proof.
-move=> A0 xA /=; have [x0|x0] := ltP x 0%R; first by rewrite (xA x0) mule0.
-by rewrite mule_ge0.
+case: (ltP x 0%R) => [x_lt0 ? ->|x_ge0 fx_ge0 _] //; last exact: mule_ge0.
+by rewrite mule0.
 Qed.
 
 Lemma nnfun_muleindic_ge0 d (T : sigmaRingType d) (R : realDomainType)
@@ -717,11 +712,11 @@ Proof. by rewrite sintegralE fsume_ge0// => r _; exact: nnsfun_mulemu_ge0. Qed.
 
 Lemma sintegral_indic (A : set T) : sintegral mu \1_A = mu A.
 Proof.
-rewrite sintegralE (fsbig_widen _ [set 0%R; 1%R]) => //; last 2 first.
+rewrite sintegralE (fsbig_widen _ [set 0%R; 1%R]) => //=; last 2 first.
   - exact: image_indic_sub.
   - by move=> t [[] -> /= /preimage10->]; rewrite measure0 mule0.
-have N01 : (0 <> 1:> R)%R by move=> /esym/eqP; rewrite oner_eq0.
-rewrite fsbigU//=; last by move=> t [->]//.
+have N01 : (0 <> 1:> R)%R by apply/eqP; rewrite eq_sym oner_eq0.
+rewrite fsbigU//=; last by move=> t [->].
 rewrite !fsbig_set1 mul0e add0e mul1e.
 by rewrite preimage_indic ifT ?inE// ifN ?notin_setE.
 Qed.
@@ -732,8 +727,8 @@ Lemma sintegralEnnsfun (f : {nnsfun T >-> R}) : sintegral mu f =
 Proof.
 rewrite (fsbig_widen _ setT) ?sintegralET//.
 move=> x [_ /=]; case: ltgtP => //= [xlt0 _|<-]; last by rewrite mul0e.
-rewrite preimage10 ?measure0 ?mule0//= => -[t _].
-by apply/eqP; apply: contra_ltN xlt0 => /eqP<-.
+rewrite preimage10 ?measure0 ?mule0//= => -[t _ xE].
+by apply/negP: xlt0; rewrite -leNgt -xE.
 Qed.
 
 End sintegral_lemmas.
@@ -755,14 +750,10 @@ Lemma sintegralrM : sintegral m (cst r \* f)%R = r%:E * sintegral m f.
 Proof.
 have [->|r0] := eqVneq r 0%R.
   by rewrite mul0e (eq_sintegral (cst 0%R)) ?sintegral0// => x/=; rewrite mul0r.
-rewrite !sintegralET.
-transitivity (\sum_(x \in [set: R]) x%:E * m (f @^-1` [set x / r])).
-  by under eq_fsbigr do rewrite preimage_cstM//.
-transitivity (\sum_(x \in [set: R]) r%:E * (x%:E * m (f @^-1` [set x]))).
-  rewrite (reindex_fsbigT (fun x => r * x)%R)//; last first.
-    by exists ( *%R r ^-1)%R; [exact: mulKf|exact: mulVKf].
-  by apply: eq_fsbigr => x; rewrite mulrAC divrr ?unitfE// mul1r muleA EFinM.
-by rewrite ge0_mule_fsumr// => x; exact: nnsfun_mulemu_ge0.
+rewrite !sintegralET ge0_mule_fsumr; last exact: nnsfun_mulemu_ge0.
+rewrite (reindex_fsbigT ( *%R r))/=; last first.
+  by exists ( *%R r^-1); [exact: mulKf|exact: mulVKf].
+by apply: eq_fsbigr => x; rewrite preimage_cstM// [_ / r]mulrC mulKf// muleA.
 Qed.
 
 End sintegralrM.
@@ -783,7 +774,7 @@ transitivity (\sum_(z \in FG) z%:E * \sum_(a \in F) m (pf a `&` pg (z - a)%R)).
   apply: eq_fsbigr => z _; rewrite preimage_add -fsbig_setU// measure_fsbig//.
     by move=> x Fx; exact: measurableI.
   exact/trivIset_setIr/trivIset_preimage1.
-under eq_fsbigr do rewrite ge0_mule_fsumr//; rewrite exchange_fsbig//.
+under eq_fsbigr do rewrite ge0_mule_fsumr//; rewrite exchange_fsbig//=.
 transitivity (\sum_(x \in F) \sum_(y \in G) (x + y)%:E * m (pf x `&` pg y)).
   apply: eq_fsbigr => x _; rewrite /pf /pg (fsbig_widen G setT)//=; last first.
     by move=> y [_ /= /preimage10->]; rewrite setI0 measure0 mule0.
diff --git a/theories/separation_axioms.v b/theories/separation_axioms.v
index c136e2bfd..89a01e9d6 100644
--- a/theories/separation_axioms.v
+++ b/theories/separation_axioms.v
@@ -845,12 +845,10 @@ move: x e1 e2; elim: n.
   move=> x e1 e2 e1e2 y [?] gxy; split; first exact: (lt_le_trans _ e1e2).
   by apply: descendG; last (exact: gxy); exact: distN_le.
 move=> n IH x e1 e2 e1e2 z [y] [d1] [d2] [] /IH P d1pos d2pos gyz d1d2e1.
-have d1e1d2 : d1 = e1 - d2 by rewrite -d1d2e1 -addrA subrr addr0.
-have e2d2le : e1 - d2 <= e2 - d2 by exact: lerB.
 exists y, (e2 - d2), d2; split => //.
-- by apply: P; apply: le_trans e2d2le; rewrite d1e1d2.
-- by apply: lt_le_trans e2d2le; rewrite -d1e1d2.
-- by rewrite -addrA [-_ + _]addrC subrr addr0.
+- by apply: P; rewrite lerBrDr d1d2e1.
+- by apply: lt_le_trans d1pos _; rewrite lerBrDr d1d2e1.
+- by rewrite subrK.
 Qed.
 
 Local Lemma step_ball_le x e1 e2 :
@@ -901,15 +899,13 @@ case: (pselect (e2 <= d2)).
     by rewrite -deE lerDr; exact: ltW.
   - exact: n_step_ball_center.
   - by rewrite addn0.
-have d1E' : d1 = e1 + (e2 - d2).
-  by move: deE; rewrite addrA [e1 + _]addrC => <-; rewrite -addrA subrr addr0.
+have d1E' : d1 = e1 + (e2 - d2) by rewrite addrA -deE addrK.
 move=> /negP; rewrite -ltNge// => d2lee2.
   case: (IH e1 (e2 - d2) x y); rewrite ?subr_gt0 // -d1E' //.
   move=> t1 [t2] [c1] [c2] [] Oxy1 gt1t2 t2y <-.
   exists t1, t2, c1, c2.+1; split => //.
   - by apply: (@n_step_ball_le _ _ d1); rewrite -?deE // ?lerDl; exact: ltW.
-  - exists y, (e2 - d2), d2; split; rewrite // ?subr_gt0//.
-    by rewrite -addrA [-_ + _]addrC subrr addr0.
+  - by exists y, (e2 - d2), d2; split; rewrite // ?subr_gt0// subrK.
   - by rewrite addnS.
 Qed.
 
diff --git a/theories/sequences.v b/theories/sequences.v
index 1e803af79..a3017a06d 100644
--- a/theories/sequences.v
+++ b/theories/sequences.v
@@ -563,7 +563,7 @@ Proof. by rewrite seriesEnat/= -big_cat_nat// leq_addl. Qed.
 
 Lemma sub_series_geq m n : (m <= n)%N ->
   series n - series m = \sum_(m <= k < n) u_ k.
-Proof. by move=> /subnK<-; rewrite series_addn addrAC subrr add0r. Qed.
+Proof. by move=> /subnK<-; rewrite series_addn addrC addKr. Qed.
 
 Lemma sub_series m n :
   series n - series m = if (m <= n)%N then \sum_(m <= k < n) u_ k
@@ -3112,7 +3112,7 @@ have majball : forall f x, F f -> (ball x0 r%:num) x -> `|f (x - x0)| <= n%:R +
   apply/(le_trans (ler_normB _ _))/lerD; first exact: majballi.
   by apply: majballi => //; exact/ball_center.
 have ballprop : ball x0 r%:num (2^-1 * (r%:num / `|y|) *: y  + x0).
-  rewrite -ball_normE /ball_ /= opprD addrCA subrr addr0 normrN normrZ.
+  rewrite -ball_normE /ball_ /= opprD addrC subrK normrN normrZ.
   rewrite 2!normrM -2!mulrA (@normfV _ `|y|) normr_id mulVf ?mulr1 ?normr_eq0//.
   by rewrite gtr0_norm // gtr0_norm // gtr_pMl // invf_lt1 // ltr1n.
 have := majball f (2^-1 * (r%:num / `|y|) *: y + x0) Ff ballprop.
diff --git a/theories/topology_theory/num_topology.v b/theories/topology_theory/num_topology.v
index ea3c2194d..ea87ef618 100644
--- a/theories/topology_theory/num_topology.v
+++ b/theories/topology_theory/num_topology.v
@@ -44,21 +44,18 @@ case => [][[[]l|[]]] [[]r|[]] [[]]//= _.
   apply/(subset_trans _ lrU)/subset_ball_prop_in_itv.
   suff : (`]x - Order.min (x - l) (r - x), x + Order.min (x - l) (r - x)[
           <= `]l, r[)%O by move/subitvP => H ? ?; exact: H.
-  apply/andP; rewrite lteBSide; split => /=.
-    apply: (@le_trans _ _ (x - (x - l))); last by rewrite lerB // ge_min lexx.
-    by rewrite opprB addrCA subrr addr0.
-  apply: (@le_trans _ _ (x + (r - x))); last by rewrite addrCA subrr addr0.
-  by rewrite lerD // ge_min lexx orbT.
+  rewrite subitvE 2!lteBSide/=.
+  by rewrite lerBrDl [_ + l]addrC -2!lerBrDl 2!ge_min 2!lexx orbT.
 - move=> xl lU; exists (x - l) => /=; first by rewrite lterBDr add0r (itvP xl).
   apply/(subset_trans _ lU)/subset_ball_prop_in_itv.
   suff : (`]x - (x - l), x + (x - l)[ <= `]l, +oo[)%O.
     by move/subitvP => H ?; exact: H.
-  by apply/andP; rewrite lteBSide/=; split; rewrite // opprB addrCA subrr addr0.
+  by rewrite subitvE lteBSide/= subKr lexx.
 - move=> xr rU; exists (r - x) => /=; first by rewrite lterBDr add0r (itvP xr).
   apply/(subset_trans _ rU)/subset_ball_prop_in_itv.
   suff : (`]x - (r - x), x + (r - x)[ <= `]-oo, r[)%O.
     by move/subitvP => H ?; exact: H.
-  by apply/andP; rewrite lteBSide/=; split; rewrite // addrCA subrr addr0.
+  by rewrite subitvE lteBSide/= addrC subrK.
 - by move=> _; rewrite set_itvE subTset => ->; exists 1 => /=.
 Qed.
 
diff --git a/theories/trigo.v b/theories/trigo.v
index 39bebecc9..90a2d0435 100644
--- a/theories/trigo.v
+++ b/theories/trigo.v
@@ -838,7 +838,7 @@ Lemma cos2_tan2 x : cos x != 0 -> (cos x) ^- 2 = 1 + (tan x) ^+ 2.
 Proof.
 move=> cosx.
 rewrite /tan exprMn [X in _ = 1 + X * _]sin2cos2 mulrBl -exprMn divff //.
-by rewrite expr1n addrCA subrr addr0 mul1r exprVn.
+by rewrite expr1n addrC subrK mul1r exprVn.
 Qed.
 
 Lemma tan_pihalf : tan (pi / 2) = 0.
diff --git a/theories/tvs.v b/theories/tvs.v
index d03357bef..cb5c93eaf 100644
--- a/theories/tvs.v
+++ b/theories/tvs.v
@@ -113,16 +113,16 @@ Lemma nbhsT_subproof (f : continuous (fun x : E * E => x.1 + x.2)) (x : E) :
 Proof.
 move => U0; have /= := f (x, -x) U; rewrite subrr => /(_ U0).
 move=> [B] [B1 B2] BU; near=> x0.
-exists (x0 - x); last by rewrite addrCA subrr addr0.
+exists (x0 - x); last by rewrite addrC subrK.
 by apply: (BU (x0, -x)); split; [near: x0; rewrite nearE|exact: nbhs_singleton].
 Unshelve. all: by end_near. Qed.
 
 Lemma nbhsB_subproof (f : continuous (fun x : E * E => x.1 + x.2)) (z x : E) :
   nbhs z U -> nbhs (x + z) (+%R x @` U).
 Proof.
-move=> U0; have /= := f (x + z, -x) U; rewrite addrAC subrr add0r.
+move=> U0; have /= := f (x + z, -x) U; rewrite [x + z]addrC addrK.
 move=> /(_ U0)[B] [B1 B2] BU; near=> x0.
-exists (x0 - x); last by rewrite addrCA subrr addr0.
+exists (x0 - x); last by rewrite addrC subrK.
 by apply: (BU (x0, -x)); split; [near: x0; rewrite nearE|exact: nbhs_singleton].
 Unshelve. all: by end_near. Qed.
 
@@ -143,42 +143,39 @@ Definition entourage : set_system (E * E) :=
                      (forall xy : E * E,  (xy.1 - xy.2) \in U -> xy \in P).
 
 Let nbhs0N (U : set E) : nbhs (0 : E) U -> nbhs (0 : E) (-%R @` U).
-Proof. by apply: nbhs0N_subproof; exact: scale_continuous. Qed.
+Proof. exact/nbhs0N_subproof/scale_continuous. Qed.
 
 Lemma nbhsN (U : set E) (x : E) : nbhs x U -> nbhs (-x) (-%R @` U).
-Proof. by apply: nbhsN_subproof; exact: scale_continuous. Qed.
+Proof. exact/nbhsN_subproof/scale_continuous. Qed.
 
 Let nbhsT (U : set E) (x : E) : nbhs (0 : E) U -> nbhs x (+%R x @`U).
-Proof. by apply: nbhsT_subproof; exact: add_continuous. Qed.
+Proof. exact/nbhsT_subproof/add_continuous. Qed.
 
 Let nbhsB (U : set E) (z x : E) : nbhs z U -> nbhs (x + z) (+%R x @`U).
-Proof. by apply: nbhsB_subproof; exact: add_continuous. Qed.
+Proof. exact/nbhsB_subproof/add_continuous. Qed.
 
 Lemma entourage_filter : Filter entourage.
 Proof.
-split; first by exists [set: E]; split => //; exact: filter_nbhsT.
-- move=> P Q; rewrite /entourage nbhsE //=.
+split; first by exists [set: E]; split; first exact: filter_nbhsT.
+  move=> P Q; rewrite /entourage nbhsE /=.
   move=> [U [[B B0] BU Bxy]] [V [[C C0] CV Cxy]].
-  exists (U `&` V); split.
+  exists (U `&` V); split => [|xy].
     by exists (B `&` C); [exact: open_nbhsI|exact: setISS].
-  move=> xy; rewrite !in_setI => /andP[xyU xyV].
-  by apply/andP;split; [exact: Bxy|exact: Cxy].
-- move=> P Q PQ; rewrite /entourage /= => [[U [HU Hxy]]]; exists U; split=> //.
-  by move => xy /Hxy /[!inE] /PQ.
+  by rewrite !in_setI => /andP[/Bxy-> /Cxy->].
+by move=> P Q PQ [U [HU Hxy]]; exists U; split=> [|xy /Hxy /[!inE] /PQ].
 Qed.
 
 Local Lemma entourage_refl (A : set (E * E)) :
   entourage A -> [set xy | xy.1 = xy.2] `<=` A.
 Proof.
-rewrite /entourage => -[/= U [U0 Uxy]] xy /eqP; rewrite -subr_eq0 => /eqP xyE.
-by apply/set_mem/Uxy; rewrite xyE; apply/mem_set; exact: nbhs_singleton.
+move=> [U [U0 Uxy]] xy eq_xy; apply/set_mem/Uxy; rewrite eq_xy subrr.
+apply/mem_set; exact: nbhs_singleton.
 Qed.
 
-Local Lemma entourage_inv :
-  forall A : set (E * E), entourage A -> entourage A^-1%relation.
+Local Lemma entourage_inv (A : set (E * E)) :
+  entourage A -> entourage A^-1%relation.
 Proof.
-move=> A [/= U [U0 Uxy]]; rewrite /entourage /=.
-exists (-%R @` U); split; first exact: nbhs0N.
+move=> [/= U [U0 Uxy]]; exists (-%R @` U); split; first exact: nbhs0N.
 move=> xy /set_mem /=; rewrite -opprB => [[yx] Uyx] /oppr_inj yxE.
 by apply/Uxy/mem_set; rewrite /= -yxE.
 Qed.
@@ -205,21 +202,20 @@ rewrite /nbhs_ /=; apply/funext => x; rewrite /filter_from/=.
 apply/funext => U; apply/propext => /=; rewrite /entourage /=; split.
 - pose V : set E := [set v | x - v \in U].
   move=> nU; exists [set xy | xy.1 - xy.2 \in V]; last first.
-    by move=> y /xsectionP; rewrite /V /= !inE /= opprB addrCA subrr addr0 inE.
-  exists V; split => /=; last first.
-    by move=> xy; rewrite !inE=> Vxy; rewrite /= !inE.
+    by move=> y /xsectionP; rewrite /V /= !inE /= opprB addrC subrK inE.
+  exists V; split; last by move=> xy; rewrite !inE /= inE.
   have /= := nbhsB x (nbhsN nU); rewrite subrr /= /V.
   rewrite [X in nbhs _ X -> _](_ : _ = [set v | x - v \in U])//.
   apply/funext => /= v /=; rewrite inE; apply/propext; split.
-    by move=> [x0 [x1]] Ux1 <- <-; rewrite opprB addrCA subrr addr0.
-  move=> Uxy; exists (v - x); last by rewrite addrCA subrr addr0.
-  by exists (x - v) => //; rewrite opprB.
+    by move=> [x0 [x1]] Ux1 <- <-; rewrite opprB addrC subrK.
+  move=> Uxy; exists (v - x); last by rewrite addrC subrK.
+  by exists (x - v); rewrite ?opprB.
 - move=> [A [U0 [nU UA]] H]; near=> z; apply: H; apply/xsectionP/set_mem/UA.
   near: z; rewrite nearE; have := nbhsT x (nbhs0N nU).
   rewrite [X in nbhs _ X -> _](_ : _ = [set v | x - v \in U0])//.
   apply/funext => /= z /=; apply/propext; split.
-  move=> [x0] [x1 Ux1 <-] <-; rewrite -opprB addrAC subrr add0r inE opprK//.
-  rewrite inE => Uxz; exists (z - x); last by rewrite addrCA subrr addr0.
+    by move=> [x0] [x1 Ux1 <-] <-; rewrite opprB addrC subrK inE.
+  rewrite inE => Uxz; exists (z - x); last by rewrite addrC subrK.
   by exists (x - z); rewrite ?opprB.
 Unshelve. all: by end_near. Qed.
 
@@ -286,22 +282,18 @@ move=> [k x]; apply/cvg_ballP => e le0 /=.
 pose M : R := maxr (`|e| + 1) (maxr `|k| (`|x| + `|x| + 2^-1 + 1)).
 have M0l : 0 < `|e| + 1 by rewrite ltr_wpDl.
 have M0r : 0 < maxr `|k| (`|x| + `|x| + 2^-1 + 1).
-  rewrite /maxr; case: ifPn => //.
-  have [->|k0 _] := eqVneq k 0; last by rewrite normr_gt0.
-  rewrite normr0 -ltrBlDr sub0r ltxx => /negbTE <-.
-  by rewrite (lt_le_trans (@ltrN10 _)).
-have M0 : 0 < M.
-  by have /= -> := num_lt_max 0 (PosNum M0l) (PosNum M0r); rewrite M0l.
+  rewrite comparable_lt_max; last exact/real_comparable.
+  by rewrite normr_gt0; case: eqP => /=.
 have Me : `|e| < M.
   rewrite (@lt_le_trans _ _ (`|e| + 1)) ?ltrDl//.
   have /= -> := num_le_max (`|e| + 1) (PosNum M0l) (PosNum M0r).
   by rewrite lexx.
+have M0 : 0 < M by apply: le_lt_trans Me.
 pose r := `|e| / 2 / M.
-exists (ball k r, ball x r).
-  by split; exists r => //=; rewrite !divr_gt0// normr_gt0 gt_eqF.
-move=> /= [z1 z2] [k1r k2r].
+exists (ball k r, ball x r) => [|[z1 z2] [k1r k2r]].
+  by split; exists r; rewrite //= ?divr_gt0 //= normr_gt0 gt_eqF.
 have := @ball_split _ _ (k * z2)  (k * x)  (z1 * z2) `|e|.
-rewrite /ball /= /= real_lter_normr ?gtr0_real//.
+rewrite /ball/= real_lter_normr ?gtr0_real//.
 rewrite (_ : _ < - e = false) ?orbF; last by rewrite ltr_nnorml// oppr_le0 ltW.
 apply.
   rewrite -mulrBr normrM (@le_lt_trans _ _ (M * `|x - z2|)) ?ler_wpM2r//.
@@ -336,8 +328,7 @@ Proof.
 exists [set B | exists x r, B = ball x r].
   move=> b; rewrite inE /= => [[x]] [r] -> z y l.
   rewrite !inE /ball /= => zx yx l0; rewrite -subr_gt0 => l1.
-  have -> : x = l *: x + (1 - l) *: x.
-    by rewrite scalerBl addrCA subrr addr0 scale1r.
+  have -> : x = l *: x + (1 - l) *: x by rewrite scalerBl addrC subrK scale1r.
   rewrite [X in `|X|](_ : _ = l *: (x - z) + (1 - l) *: (x - y)); last first.
     by rewrite opprD addrACA -mulrBr -mulrBr.
   rewrite (@le_lt_trans _ _ (`|l| * `|x - z| + `|1 - l| * `|x - y|))//.
@@ -346,9 +337,8 @@ exists [set B | exists x r, B = ball x r].
     rewrite ltr_leD//.
       by rewrite -ltr_pdivlMl ?mulrA ?mulVf ?mul1r // ?normrE ?gt_eqF.
     by rewrite -ler_pdivlMl ?mulrA ?mulVf ?mul1r ?ltW // ?normrE ?gt_eqF.
-  have -> : `|1 - l| = 1 - `| l |.
-    by move: l0 l1 => /ltW/normr_idP -> /ltW/normr_idP ->.
-  by rewrite -mulrDl addrCA subrr addr0 mul1r.
+  suff-> : `|1 - l| = 1 - `|l| by rewrite -mulrDl addrC subrK mul1r.
+  by move: l0 l1 => /ltW/normr_idP -> /ltW/normr_idP ->.
 split.
   move=> B [x] [r] ->.
   rewrite openE/= /ball/= /interior => y /= bxy; rewrite -nbhs_ballE.