diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 3c9ab85141..746bc12f3b 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -76,6 +76,16 @@
 	`ae_eq_mul1l`,
 	`ae_eq_abse`
 
+- moved from `derive.v` to `normedtype.v`:
+  + lemmas `cvg_at_rightE`, `cvg_at_leftE`
+
+- in `ereal.v`:
+  + definitions `ereal_dnbhs` and `ereal_nbhs` changed to use large inequality instead
+    of strict inequality
+- in `normedtype.v`:
+  + definitions `pinfty_dnbhs` and `ninfty_nbhs` changed to use large inequality instead
+    of strict inequality
+
 ### Renamed
 
 - in `exp.v`:
diff --git a/theories/derive.v b/theories/derive.v
index 3a3bbb626e..44fc014bb4 100644
--- a/theories/derive.v
+++ b/theories/derive.v
@@ -1319,8 +1319,8 @@ have imf_sup : has_sup imf.
   split; first by exists (f a); apply/imageP; rewrite /= in_itv /= lexx.
   have [M [Mreal imfltM]] : bounded_set (f @` `[a, b]).
     by apply/compact_bounded/continuous_compact => //; exact: segment_compact.
-  exists (M + 1) => y /imfltM yleM.
-  by rewrite (le_trans _ (yleM _ _)) ?ler_norm ?ltr_addl.
+  exists (M + 1); apply/ubP => y /imfltM/= yleM.
+  by rewrite (le_trans _ (yleM _ _)) ?ler_addl ?ler_norm.
 have [|imf_ltsup] := pselect (exists2 c, c \in `[a, b]%R & f c = sup imf).
   move=> [c cab fceqsup]; exists c => // t tab; rewrite fceqsup.
   by apply/sup_upper_bound => //; exact/imageP.
diff --git a/theories/ereal.v b/theories/ereal.v
index 37d007b91d..3230b1d028 100644
--- a/theories/ereal.v
+++ b/theories/ereal.v
@@ -633,17 +633,20 @@ Local Open Scope classical_set_scope.
 Definition ereal_dnbhs (x : \bar R) (P : \bar R -> Prop) : Prop :=
   match x with
     | r%:E => r^' (fun r => P r%:E)
-    | +oo => exists M, M \is Num.real /\ forall y, M%:E < y -> P y
-    | -oo => exists M, M \is Num.real /\ forall y, y < M%:E -> P y
+    | +oo => exists M, M \is Num.real /\ forall y, M%:E <= y -> P y
+    | -oo => exists M, M \is Num.real /\ forall y, y <= M%:E -> P y
   end.
+
 Definition ereal_nbhs (x : \bar R) (P : \bar R -> Prop) : Prop :=
   match x with
     | x%:E => nbhs x (fun r => P r%:E)
-    | +oo => exists M, M \is Num.real /\ forall y, M%:E < y -> P y
-    | -oo => exists M, M \is Num.real /\ forall y, y < M%:E -> P y
+    | +oo => exists M, M \is Num.real /\ forall y, M%:E <= y -> P y
+    | -oo => exists M, M \is Num.real /\ forall y, y <= M%:E -> P y
   end.
+
 Canonical ereal_ereal_filter :=
   FilteredType (extended R) (extended R) (ereal_nbhs).
+
 End ereal_nbhs.
 
 Section ereal_nbhs_instances.
@@ -652,70 +655,53 @@ Context {R : numFieldType}.
 Global Instance ereal_dnbhs_filter :
   forall x : \bar R, ProperFilter (ereal_dnbhs x).
 Proof.
-case=> [x||].
-- case: (Proper_dnbhs_numFieldType x) => x0 [//= xT xI xS].
-  apply Build_ProperFilter' => //=; apply Build_Filter => //=.
-  move=> P Q lP lQ; exact: xI.
-  by move=> P Q PQ /xS; apply => y /PQ.
-- apply Build_ProperFilter.
-    move=> P [x [xr xP]] //; exists (x + 1)%:E; apply xP => /=.
-    by rewrite lte_fin ltr_addl.
-  split=> /= [|P Q [MP [MPr gtMP]] [MQ [MQr gtMQ]] |P Q sPQ [M [Mr gtM]]].
+move=> [r| |].
+- by apply: Build_ProperFilter' => //=; exact: filter_not_empty.
+- apply: Build_ProperFilter => [P [x [_ xP]]|].
+    by exists x%:E; exact: xP.
+  apply: Build_Filter => /= [|P Q [r +] [s +] |P Q PQ [r [rr rP]]].
   + by exists 0%R.
-  + have [MP0|MP0] := eqVneq MP 0%R.
-      have [MQ0|MQ0] := eqVneq MQ 0%R.
-        by exists 0%R; split => // x x0; split;
-          [apply/gtMP; rewrite MP0 | apply/gtMQ; rewrite MQ0].
-      exists `|MQ|%R; rewrite realE normr_ge0; split => // x MQx; split.
-        by apply: gtMP; rewrite (le_lt_trans _ MQx) // MP0 lee_fin.
-      by apply gtMQ; rewrite (le_lt_trans _ MQx)// lee_fin real_ler_normr ?lexx.
-    have [MQ0|MQ0] := eqVneq MQ 0%R.
-      exists `|MP|%R; rewrite realE normr_ge0; split => // x MPx; split.
-      by apply gtMP; rewrite (le_lt_trans _ MPx)// lee_fin real_ler_normr ?lexx.
-      by apply gtMQ; rewrite (le_lt_trans _ MPx) // lee_fin MQ0.
-    have {}MP0 : (0 < `|MP|)%R by rewrite normr_gt0.
-    have {}MQ0 : (0 < `|MQ|)%R by rewrite normr_gt0.
-    exists (Num.max (PosNum MP0) (PosNum MQ0))%:num.
-    rewrite realE /= ge0 /=; split => //.
-    case=> [r| |//].
-    * rewrite lte_fin/= num_max num_lt_maxl /= => /andP[MPx MQx]; split.
-      by apply/gtMP; rewrite lte_fin (le_lt_trans _ MPx)// real_ler_normr ?lexx.
-      by apply/gtMQ; rewrite lte_fin (le_lt_trans _ MQx)// real_ler_normr ?lexx.
-    * by move=> _; split; [apply/gtMP | apply/gtMQ].
-  + by exists M; split => // ? /gtM /sPQ.
-- apply Build_ProperFilter.
-  + move=> P [M [Mr ltMP]]; exists (M - 1)%:E.
-    by apply: ltMP; rewrite lte_fin gtr_addl oppr_lt0.
-  + split=> /= [|P Q [MP [MPr ltMP]] [MQ [MQr ltMQ]] |P Q sPQ [M [Mr ltM]]].
+  + have [-> [_ rP] [sr sQ]|r0 [rr rP]] := eqVneq r 0%R.
+      exists `|s|%R; rewrite normr_real; split => // x sx; split.
+        exact/rP/(le_trans _ sx).
+      by apply/sQ/(le_trans _ sx); rewrite lee_fin real_ler_normr ?lexx.
+    have [-> [_ sQ]|s0 [sr sQ]] := eqVneq s 0%R.
+      exists `|r|%R; rewrite normr_real; split => // x rx; split.
+        by apply/rP/(le_trans _ rx); rewrite lee_fin real_ler_normr ?lexx.
+      exact/sQ/(le_trans _ rx).
+    have /andP[{}r0 {}s0]: ((0 < `|r|) && (0 < `|s|))%R by rewrite !normr_gt0 r0.
+    exists (Num.max (PosNum r0) (PosNum s0))%:num.
+    rewrite realE /= ge0 /=; split => // -[t|_|//].
+    * rewrite lee_fin /= num_max num_le_maxl /= => /andP[rx sx]; split.
+        by apply/rP; rewrite lee_fin (le_trans _ rx)// real_ler_normr ?lexx.
+      by apply/sQ; rewrite lee_fin (le_trans _ sx)// real_ler_normr ?lexx.
+    * by split; [exact/rP|exact/sQ].
+  + by exists r; split => // ? /rP /PQ.
+- apply: Build_ProperFilter => [P [x [_ xP]]|].
+  + by exists (x - 1)%:E; apply: xP; rewrite lee_fin ger_addl.
+  + split=> /= [|P Q [r +] [s +] |P Q PQ [r [rr rP]]].
     * by exists 0%R.
-    * have [MP0|MP0] := eqVneq MP 0%R.
-        have [MQ0|MQ0] := eqVneq MQ 0%R.
-          by exists 0%R; split => // x x0; split;
-          [apply/ltMP; rewrite MP0 | apply/ltMQ; rewrite MQ0].
-        exists (- `|MQ|)%R; rewrite realN realE normr_ge0; split => // x xMQ.
-        split.
-          by apply ltMP; rewrite (lt_le_trans xMQ)// lee_fin MP0 ler_oppl oppr0.
-       apply ltMQ; rewrite (lt_le_trans xMQ) // lee_fin ler_oppl -normrN.
-       by rewrite real_ler_normr ?realN // lexx.
-    * have [MQ0|MQ0] := eqVneq MQ 0%R.
-        exists (- `|MP|)%R; rewrite realN realE normr_ge0; split => // x MPx.
-        split.
-          apply ltMP; rewrite (lt_le_trans MPx) // lee_fin ler_oppl -normrN.
-          by rewrite real_ler_normr ?realN // lexx.
-        by apply ltMQ; rewrite (lt_le_trans MPx) // lee_fin MQ0 ler_oppl oppr0.
-      have {}MP0 : (0 < `|MP|)%R by rewrite normr_gt0.
-      have {}MQ0 : (0 < `|MQ|)%R by rewrite normr_gt0.
-      exists (- (Num.max (PosNum MP0) (PosNum MQ0))%:num)%R.
-      rewrite realN realE /= ge0 /=; split => //.
-      case=> [r|//|].
-      - rewrite lte_fin ltr_oppr num_max num_lt_maxl => /andP[].
-        rewrite ltr_oppr => MPx; rewrite ltr_oppr => MQx; split.
-          apply/ltMP; rewrite lte_fin (lt_le_trans MPx) //= ler_oppl -normrN.
+    * have [-> [_ rP] [sr sQ]|r0 [rr rP]] := eqVneq r 0%R.
+        exists (- `|s|)%R; rewrite realN normr_real; split => // x xs; split.
+          by apply/rP/(le_trans xs); rewrite lee_fin ler_oppl oppr0.
+        apply/sQ/(le_trans xs); rewrite lee_fin ler_oppl -normrN.
+        by rewrite real_ler_normr ?realN ?lexx.
+      have [-> [_ sQ]|s0 [sr sQ]] := eqVneq s 0%R.
+        exists (- `|r|)%R; rewrite realN normr_real; split => // x rx; split.
+          apply/rP/(le_trans rx); rewrite lee_fin ler_oppl -normrN.
           by rewrite real_ler_normr ?realN // lexx.
-        apply/ltMQ; rewrite lte_fin (lt_le_trans MQx) //= ler_oppl -normrN.
-        by rewrite real_ler_normr ?realN // lexx.
-      - by move=> _; split; [apply/ltMP | apply/ltMQ].
-    * by exists M; split => // x /ltM /sPQ.
+        by apply/sQ/(le_trans rx); rewrite lee_fin ler_oppl oppr0.
+    have /andP[{}r0 {}s0]: ((0 < `|r|) && (0 < `|s|))%R by rewrite !normr_gt0 r0.
+      exists (- (Num.max (PosNum r0) (PosNum s0))%:num)%R.
+      rewrite realN realE /= ge0 /=; split => // -[t|//|_].
+      - rewrite lee_fin ler_oppr num_max num_le_maxl => /andP[].
+        rewrite ler_oppr => rx; rewrite ler_oppr => sx; split.
+          apply/rP; rewrite lee_fin (le_trans rx) //= ler_oppl -normrN.
+          by rewrite real_ler_normr ?realN ?lexx.
+        apply/sQ; rewrite lee_fin (le_trans sx) //= ler_oppl -normrN.
+        by rewrite real_ler_normr ?realN ?lexx.
+      - by split; [exact/rP|exact/sQ].
+    * by exists r; split => // ? /rP /PQ.
 Qed.
 Typeclasses Opaque ereal_dnbhs.
 
@@ -737,13 +723,19 @@ Context (R : numFieldType).
 Implicit Type (r : R).
 
 Lemma ereal_nbhs_pinfty_gt r : r \is Num.real -> \forall x \near +oo, r%:E < x.
-Proof. by exists r. Qed.
+Proof.
+exists (r + 1)%R; split=> [|y]; first by rewrite realD.
+by apply: lt_le_trans; rewrite EFinD lte_fin ltr_addl.
+Qed.
 
 Lemma ereal_nbhs_pinfty_ge r : r \is Num.real -> \forall x \near +oo, r%:E <= x.
 Proof. by exists r; split => //; apply: ltW. Qed.
 
 Lemma ereal_nbhs_ninfty_lt r : r \is Num.real -> \forall x \near -oo, r%:E > x.
-Proof. by exists r. Qed.
+Proof.
+exists (r - 1)%R; split=> [|y]; first by rewrite realB.
+by move=> /le_lt_trans; apply; rewrite lte_fin ltr_subl_addl ltr_addr.
+Qed.
 
 Lemma ereal_nbhs_ninfty_le r : r \is Num.real -> \forall x \near -oo, r%:E >= x.
 Proof. by exists r; split => // ?; apply: ltW. Qed.
@@ -780,32 +772,34 @@ move: p => -[p| [M [Mreal MA]] | [M [Mreal MA]]] //=.
   apply/nbhs_ballP; exists (e%:num / 2) => //= r per.
   apply/nbhs_ballP; exists (e%:num / 2) => //= x rex.
   apply/ballA/(@ball_splitl _ _ r) => //; exact/ball_sym.
-- exists (M + 1)%R; split; first by rewrite realD.
-  move=> -[x| _ |_] //=; last by exists M.
-  rewrite lte_fin => M'x /=.
-  apply/nbhs_ballP; exists 1%R => //= y x1y.
-  apply MA; rewrite lte_fin.
-  rewrite addrC -ltr_subr_addl in M'x.
-  rewrite (lt_le_trans M'x) // ler_subl_addl addrC -ler_subl_addl.
-  rewrite (le_trans _ (ltW x1y)) // real_ler_norm // realB //.
-    rewrite ltr_subr_addr in M'x.
-    rewrite -comparabler0 (@comparabler_trans _ (M + 1)%R) //.
-      by rewrite /Order.comparable (ltW M'x) orbT.
-    by rewrite comparabler0 realD.
-  by rewrite num_real. (* where we really use realFieldType *)
-- exists (M - 1)%R; split; first by rewrite realB.
-  move=> -[x| _ |_] //=; last by exists M.
-  rewrite lte_fin => M'x /=.
-  apply/nbhs_ballP; exists 1%R => //= y x1y.
-  apply MA; rewrite lte_fin.
-  rewrite ltr_subr_addl in M'x.
-  rewrite (le_lt_trans _ M'x) // addrC -ler_subl_addl.
-  rewrite (le_trans _ (ltW x1y)) // distrC real_ler_norm // realB //.
+- exists (M + 1)%R; split; first by rewrite realD // real1.
+  move=> -[x| _ |] //=.
+    rewrite lee_fin => M'x /=.
+    apply/nbhs_ballP; exists 1%R => //= y x1y.
+    apply MA; rewrite lee_fin.
+    rewrite addrC -ler_subr_addl in M'x.
+    rewrite (le_trans M'x) // ler_subl_addl addrC -ler_subl_addl.
+    rewrite (le_trans _ (ltW x1y)) // real_ler_norm // realB //.
+      rewrite ler_subr_addr in M'x.
+      rewrite -comparabler0 (@comparabler_trans _ (M + 1)%R) //.
+        by rewrite /Order.comparable M'x orbT.
+      by rewrite comparabler0 realD // real1.
     by rewrite num_real. (* where we really use realFieldType *)
-  rewrite addrC -ltr_subr_addr in M'x.
-  rewrite -comparabler0 (@comparabler_trans _ (M - 1)%R) //.
-    by rewrite /Order.comparable (ltW M'x).
-  by rewrite comparabler0 realB.
+  by exists M.
+- exists (M - 1)%R; split; first by rewrite realB // real1.
+  move=> -[x| _ |] //=.
+    rewrite lee_fin => M'x /=.
+    apply/nbhs_ballP; exists 1%R => //= y x1y.
+    apply MA; rewrite lee_fin.
+    rewrite ler_subr_addl in M'x.
+    rewrite (le_trans _ M'x) // addrC -ler_subl_addl.
+    rewrite (le_trans _ (ltW x1y)) // distrC real_ler_norm // realB //.
+      by rewrite num_real. (* where we really use realFieldType *)
+    rewrite addrC -ler_subr_addr in M'x.
+    rewrite -comparabler0 (@comparabler_trans _ (M - 1)%R) //.
+      by rewrite /Order.comparable M'x.
+    by rewrite comparabler0 realB // real1.
+  by exists M.
 Qed.
 
 Definition ereal_topologicalMixin : Topological.mixin_of (@ereal_nbhs R) :=
@@ -833,19 +827,19 @@ case: x => [r /=| |].
 - rewrite predeqE => S; split=> [[M [Mreal MS]]|[x [M [Mreal Mx]] <-]].
     exists (-%E @` S).
       exists (- M)%R; rewrite realN Mreal; split => // x Mx.
-      by exists (- x); [apply MS; rewrite lte_oppl | rewrite oppeK].
+      by exists (- x); [apply MS; rewrite lee_oppl | rewrite oppeK].
     rewrite predeqE => x; split=> [[y [z Sz <- <-]]|Sx]; first by rewrite oppeK.
     by exists (- x); [exists x | rewrite oppeK].
   exists (- M)%R; rewrite realN; split => // y yM.
-  exists (- y); by [apply Mx; rewrite lte_oppr|rewrite oppeK].
+  exists (- y); by [apply Mx; rewrite lee_oppr|rewrite oppeK].
 - rewrite predeqE => S; split=> [[M [Mreal MS]]|[x [M [Mreal Mx]] <-]].
     exists (-%E @` S).
       exists (- M)%R; rewrite realN Mreal; split => // x Mx.
-      by exists (- x); [apply MS; rewrite lte_oppr | rewrite oppeK].
+      by exists (- x); [apply MS; rewrite lee_oppr | rewrite oppeK].
     rewrite predeqE => x; split=> [[y [z Sz <- <-]]|Sx]; first by rewrite oppeK.
     by exists (- x); [exists x | rewrite oppeK].
   exists (- M)%R; rewrite realN; split => // y yM.
-  exists (- y); by [apply Mx; rewrite lte_oppl|rewrite oppeK].
+  exists (- y); by [apply Mx; rewrite lee_oppl|rewrite oppeK].
 Qed.
 
 Lemma nbhsNKe (R : realFieldType) (z : \bar R) (A : set (\bar R)) :
@@ -1044,12 +1038,15 @@ Lemma nbhs_oo_up_e1 (A : set (\bar R)) (e : {posnum R}) : (e%:num <= 1)%R ->
   ereal_ball +oo e%:num `<=` A -> nbhs +oo A.
 Proof.
 move=> e1 ooeA.
-exists (fine (expand (1 - e%:num)%R)); rewrite num_real; split => //.
-case => [r | | //].
-- rewrite fine_expand; last first.
-    by rewrite ger0_norm ?ltr_subl_addl ?ltr_addr // subr_ge0.
-  by move=> ?; exact/ooeA/expand_ereal_ball_pinfty.
-- by move=> _; exact/ooeA/ereal_ball_center.
+exists (fine (expand (1 - e%:num / 2)%R)); rewrite num_real; split => //.
+have e21 : (`|1 - e%:num / 2| < 1)%R.
+  rewrite ger0_norm; first by rewrite ltr_subl_addl ltr_addr.
+  by rewrite subr_ge0 ler_pdivr_mulr// mul1r (le_trans e1)// ler1n.
+case => [r| _ |//]; last exact/ooeA/ereal_ball_center.
+rewrite fine_expand // => er; apply/ooeA/expand_ereal_ball_pinfty => //.
+rewrite (lt_le_trans _ er)// lt_expand ?inE; last exact/ltW.
+  by rewrite ler_lt_sub// ltr_pdivr_mulr// ltr_pmulr// ltr1n.
+by rewrite ger0_norm ?subr_ge0// ler_subl_addl addrC -ler_subl_addl subrr.
 Qed.
 
 Lemma nbhs_oo_down_e1 (A : set (\bar R)) (e : {posnum R}) : (e%:num <= 1)%R ->
@@ -1312,12 +1309,12 @@ rewrite predeq2E => x A; split.
       by rewrite subr_gt0 (le_lt_trans _ (contract_lt1 M)) // ler_norm.
     case=> [r| |]/=.
     * rewrite /ereal_ball [_ +oo]/= => rM1.
-      apply: MA; rewrite lte_fin.
+      apply: MA; rewrite lee_fin.
       rewrite ger0_norm in rM1; last first.
         by rewrite subr_ge0 // (le_trans _ (contract_le1 r%:E)) // ler_norm.
       rewrite ltr_subl_addr addrC addrCA addrC -ltr_subl_addr subrr in rM1.
       rewrite subr_gt0 in rM1.
-      by rewrite -lte_fin -lt_contract.
+      by rewrite -lee_fin -le_contract ltW.
     * by rewrite /ereal_ball /= subrr normr0 => h; exact: MA.
     * rewrite /ereal_ball /= opprK => h {MA}.
       exfalso.
@@ -1332,12 +1329,12 @@ rewrite predeq2E => x A; split.
     case=> [r| |].
     * rewrite /ereal_ball => /= rM1.
       apply MA.
-      rewrite lte_fin.
+      rewrite lee_fin.
       rewrite ler0_norm in rM1; last first.
         rewrite ler_subl_addl addr0 ltW //.
         by move: (contract_lt1 r); rewrite ltr_norml => /andP[].
       rewrite opprB opprK -ltr_subl_addl addrK in rM1.
-      by rewrite -lte_fin -lt_contract.
+      by rewrite -lee_fin -le_contract ltW.
     * rewrite /ereal_ball /= -opprD normrN => h {MA}.
       exfalso.
       move: h; apply/negP.
@@ -1410,13 +1407,15 @@ case: x => /= [x [_/posnumP[d] dP] |[d [dreal dP]] |[d [dreal dP]]]; last 2 firs
     have /ZnatP [N Nfloor] : floor (Num.max d 0%R) \is a Znat.
       by rewrite Znat_def floor_ge0 le_maxr lexx orbC.
     exists N.+1 => // n ltNn; apply: dP.
-    have /le_lt_trans : (d <= Num.max d 0)%R by rewrite le_maxr lexx.
-    by apply; rewrite (lt_le_trans (lt_succ_floor _))// Nfloor natr1 ler_nat.
+    have /le_trans : (d <= Num.max d 0)%R by rewrite le_maxr lexx.
+    apply; apply: le_trans (ltW (lt_succ_floor _)) _.
+    by rewrite Nfloor natr1 ler_nat.
   have /ZnatP [N Nfloor] : floor (Num.max (- d)%R 0%R) \is a Znat.
     by rewrite Znat_def floor_ge0 le_maxr lexx orbC.
-  exists N.+1 => // n ltNn; apply: dP; rewrite lte_fin ltr_oppl.
-  have /le_lt_trans : (- d <= Num.max (- d) 0)%R by rewrite le_maxr lexx.
-  by apply; rewrite (lt_le_trans (lt_succ_floor _))// Nfloor natr1 ler_nat.
+  exists N.+1 => // n ltNn; apply: dP; rewrite lee_fin ler_oppl.
+  have /le_trans : (- d <= Num.max (- d) 0)%R by rewrite le_maxr lexx.
+  apply; apply: le_trans (ltW (lt_succ_floor _)) _.
+  by rewrite Nfloor natr1 ler_nat.
 have /ZnatP [N Nfloor] : floor (d%:num^-1) \is a Znat.
   by rewrite Znat_def floor_ge0.
 exists N => // n leNn; apply: dP; last first.
diff --git a/theories/exp.v b/theories/exp.v
index 8290ad844a..f2aff633c3 100644
--- a/theories/exp.v
+++ b/theories/exp.v
@@ -65,7 +65,7 @@ apply: series_le_cvg Kzxn _ _ => [//=| /= n|].
     rewrite !normrM normr_id mulrAC mulfK // normr_eq0 expf_eq0 andbC.
     by case: ltrgt0P zLx; rewrite //= normr_lt0.
   do! (apply: ler_pmul || apply: mulr_ge0 || rewrite invr_ge0) => //.
-  by apply Kf => //; rewrite (lt_le_trans _ (ler_norm _))// ltr_addl.
+  by apply Kf => //; rewrite (le_trans _ (ler_norm _))// ler_addl.
 have F : `|z / x| < 1.
   by rewrite normrM normfV ltr_pdivr_mulr ?mul1r // (le_lt_trans _ zLx).
 rewrite (_ : (fun _ => _) = geometric `|K + 1| `|z / x|); last first.
diff --git a/theories/landau.v b/theories/landau.v
index 054abf4c61..b600c52dbd 100644
--- a/theories/landau.v
+++ b/theories/landau.v
@@ -473,8 +473,8 @@ split=> [[k k0 fOg] | [k [kreal fOg]]].
   exists k; rewrite realE (ltW k0) /=; split=> // l ltkl; move: fOg.
   by apply: filter_app; near=> x => /le_trans; apply; rewrite ler_wpmul2r // ltW.
 exists (Num.max 1 `|k + 1|) => //.
-apply: fOg; rewrite (@lt_le_trans _ _ `|k + 1|) //.
-  by rewrite (@lt_le_trans _ _ (k + 1)) ?ltr_addl // real_ler_norm ?realD.
+apply: fOg; rewrite (@le_trans _ _ `|k + 1|) //.
+  by rewrite (@le_trans _ _ (k + 1)) ?ler_addl// real_ler_norm ?realD.
 by rewrite comparable_le_maxr ?real_comparable// lexx orbT.
 Unshelve. end_near. Qed.
 
@@ -672,9 +672,11 @@ Notation "[o_ x e 'of' f ]" := (mklittleo gen_tag x f e).
 (*Printing*)
 Notation "[o '_' x e 'of' f ]" := (the_littleo _ _ (PhantomF x) f e).
 
-Lemma eqoO (F : filter_on T) (f : T -> V) (e : T -> W) :
-  [o_F e of f] =O_F e.
-Proof. by apply/eqOP; exists 0; split => // k kgt0; apply: littleoP. Qed.
+Lemma eqoO (F : filter_on T) (f : T -> V) (e : T -> W) : [o_F e of f] =O_F e.
+Proof.
+apply/eqOP; exists 1; split => // k kge1; apply: littleoP.
+by rewrite (lt_le_trans _ kge1).
+Qed.
 Hint Resolve eqoO : core.
 
 (* NB: duplicate from Section Domination *)
@@ -1109,10 +1111,10 @@ rewrite -linearB opprD addrC addrNK linearN normrN; near: y.
 suff flip : \forall k \near +oo, forall x, `|f x| <= k * `|x|.
   near +oo => k; near=> y.
   rewrite (le_lt_trans (near flip k _ _)) // -ltr_pdivl_mull; last first.
-    by near: k; exists 0.
+    by near: k; exact: nbhs_pinfty_gt.
   near: y; apply/nbhs_normP.
   eexists; last by move=> ?; rewrite /= sub0r normrN; apply.
-  by rewrite /= mulr_gt0 // invr_gt0; near: k; exists 0.
+  by rewrite /= mulr_gt0 // invr_gt0; near: k; exact: nbhs_pinfty_gt.
 have /nbhs_normP [_/posnumP[d]] := Of1.
 rewrite /cst [X in _ * X]normr1 mulr1 => fk; near=> k => y.
 case: (ler0P `|y|) => [|y0].
@@ -1125,7 +1127,7 @@ rewrite -normm_s.
 have <- : GRing.Scale.op s_law =2 s by rewrite GRing.Scale.opE.
 rewrite -linearZ fk //= distrC subr0 normrZ ger0_norm //.
 rewrite invfM mulrA mulfVK ?lt0r_neq0 // ltr_pdivr_mulr //.
-by rewrite -ltr_pdivr_mull//.
+by rewrite -ltr_pdivr_mull.
 Unshelve. all: by end_near. Qed.
 
 End Linear3.
@@ -1331,7 +1333,7 @@ rewrite (@le_trans _ _ ((k2%:num * k1%:num)^-1 * `|(W1 * W2) x|)) //.
   rewrite invrM ?unitfE ?gtr_eqF // -mulrA ler_pdivl_mull //.
   rewrite ler_pdivl_mull // (mulrA k1%:num) mulrCA (@normrM _ (W1 x)).
   by rewrite ler_pmul ?mulr_ge0 //; near: x.
-by rewrite ler_wpmul2r // ltW //.
+by rewrite ler_wpmul2r // ltW.
 Unshelve. all: by end_near. Qed.
 
 End big_omega_in_R.
@@ -1493,7 +1495,7 @@ rewrite [`|_|]normrM (@le_trans _ _ ((k2%:num * k1%:num)^-1 * `|(T1 * T2) x|)) /
   rewrite invrM ?unitfE ?gtr_eqF // -mulrA ler_pdivl_mull //.
   rewrite ler_pdivl_mull // (mulrA k1%:num) mulrCA (@normrM _ (T1 x)) ler_pmul //;
   by [rewrite mulr_ge0 //|near: x].
-by rewrite ler_wpmul2r // ltW //.
+by rewrite ler_wpmul2r // ltW.
 Unshelve. all: by end_near. Qed.
 
 End big_theta_in_R.
diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v
index 4bc3cc7998..6b51ec8564 100644
--- a/theories/lebesgue_integral.v
+++ b/theories/lebesgue_integral.v
@@ -424,7 +424,7 @@ Lemma simple_bounded (f : {sfun T >-> R}) :
 Proof.
 have /finite_seqP[r fr] := fimfunP f.
 exists (fine (\big[maxe/-oo%E]_(i <- r) `|i|%:E)).
-split; rewrite ?num_real// => x mx z _; apply/ltW/(le_lt_trans _ mx).
+split; rewrite ?num_real// => x mx z _; apply/(le_trans _ mx).
 have ? : f z \in r by have := imageT f z; rewrite fr.
 rewrite -[leLHS]/(fine `|f z|%:E) fine_le//.
   have := @bigmaxe_fin_num _ (map normr r) `|f z|.
@@ -4762,7 +4762,7 @@ Proof.
 move=> Afin mfA bdA; apply/integrableP; split; first exact/EFin_measurable_fun.
 have [M [_ mrt]] := bdA; apply: le_lt_trans.
   apply: (integral_le_bound (`|M| + 1)%:E) => //; first exact: measurableT_comp.
-  by apply: aeW => z Az; rewrite lee_fin mrt// ltr_spaddr// ler_norm.
+  by apply: aeW => z Az; rewrite lee_fin mrt// ler_paddr// ler_norm.
 by rewrite lte_mul_pinfty.
 Qed.
 
@@ -4854,7 +4854,7 @@ Lemma compact_finite_measure (A : set R^o) : compact A -> mu A < +oo.
 Proof.
 move=> /[dup]/compact_measurable => mA /compact_bounded[N [_ N1x]].
 have AN1 : (A `<=` `[- (`|N| + 1), `|N| + 1])%R.
-  by move=> z Az; rewrite set_itvcc /= -ler_norml N1x// ltr_spaddr// ler_norm.
+  by move=> z Az; rewrite set_itvcc /= -ler_norml N1x// ler_paddr// ler_norm.
 rewrite (le_lt_trans (le_measure _ _ _ AN1)) ?inE//=.
 by rewrite lebesgue_measure_itv/= lte_fin gtr_opp// EFinD ltry.
 Qed.
@@ -4913,7 +4913,7 @@ have mg : measurable_fun E g.
 have [M Mpos Mbd] : (exists2 M, 0 < M & forall x, `|g x| <= M)%R.
   have [M [_ /= bdM]] := simple_bounded g.
   exists (`|M| + 1)%R; first exact: ltr_spaddr.
-  by move=> x; rewrite bdM// ltr_spaddr// ler_norm.
+  by move=> x; rewrite bdM// ler_paddr// ler_norm.
 have [] // := @measurable_almost_continuous _ _ mE _ g (eps%:num / 2 / (M *+ 2)).
   by rewrite divr_gt0// mulrn_wgt0.
 move=> A [cptA AE /= muAE ctsAF].
@@ -4927,7 +4927,7 @@ move=> h [gh ctsh hbdM]; have mh : measurable_fun E h.
 have intg : mu.-integrable E (EFin \o h).
   apply: measurable_bounded_integrable => //.
   exists M; split; rewrite ?num_real // => x Mx y _ /=.
-  by rewrite (le_trans _ (ltW Mx)).
+  by rewrite (le_trans _ Mx).
 exists h; split => //; rewrite [eps%:num]splitr; apply: le_lt_trans.
   pose fgh x := `|(f x - g x)%:E| + `|(g x - h x)%:E|.
   apply: (@ge0_le_integral _ _ _ mu _ mE _ fgh) => //.
diff --git a/theories/normedtype.v b/theories/normedtype.v
index 7b871baf91..6cbcb9a8c0 100644
--- a/theories/normedtype.v
+++ b/theories/normedtype.v
@@ -438,10 +438,10 @@ Qed.
 (** * Some Topology on extended real numbers *)
 
 Definition pinfty_nbhs (R : numFieldType) : set (set R) :=
-  fun P => exists M, M \is Num.real /\ forall x, M < x -> P x.
+  fun P => exists M, M \is Num.real /\ forall x, M <= x -> P x.
 Arguments pinfty_nbhs R : clear implicits.
 Definition ninfty_nbhs (R : numFieldType) : set (set R) :=
-  fun P => exists M, M \is Num.real /\ forall x, x < M -> P x.
+  fun P => exists M, M \is Num.real /\ forall x, x <= M -> P x.
 Arguments ninfty_nbhs R : clear implicits.
 
 Notation "+oo_ R" := (pinfty_nbhs [numFieldType of R])
@@ -460,11 +460,11 @@ Implicit Types r : R.
 Global Instance proper_pinfty_nbhs : ProperFilter (pinfty_nbhs R).
 Proof.
 apply Build_ProperFilter.
-  by move=> P [M [Mreal MP]]; exists (M + 1); apply MP; rewrite ltr_addl.
+  by move=> P [M [Mreal MP]]; exists (M + 1); apply MP; rewrite ler_addl.
 split=> /= [|P Q [MP [MPr gtMP]] [MQ [MQr gtMQ]] |P Q sPQ [M [Mr gtM]]].
 - by exists 0.
 - exists (maxr MP MQ); split=> [|x]; first exact: max_real.
-  by rewrite comparable_lt_maxl ?real_comparable // => /andP[/gtMP ? /gtMQ].
+  by rewrite comparable_le_maxl ?real_comparable // => /andP[/gtMP ? /gtMQ].
 - by exists M; split => // ? /gtM /sPQ.
 Qed.
 
@@ -472,25 +472,31 @@ Global Instance proper_ninfty_nbhs : ProperFilter (ninfty_nbhs R).
 Proof.
 apply Build_ProperFilter.
   move=> P [M [Mr ltMP]]; exists (M - 1).
-  by apply: ltMP; rewrite gtr_addl oppr_lt0.
+  by apply: ltMP; rewrite ler_subl_addl ler_addr.
 split=> /= [|P Q [MP [MPr ltMP]] [MQ [MQr ltMQ]] |P Q sPQ [M [Mr ltM]]].
 - by exists 0.
 - exists (Num.min MP MQ); split=> [|x]; first exact: min_real.
-  by rewrite comparable_lt_minr ?real_comparable // => /andP[/ltMP ? /ltMQ].
+  by rewrite comparable_le_minr ?real_comparable // => /andP[/ltMP ? /ltMQ].
 - by exists M; split => // x /ltM /sPQ.
 Qed.
 
 Lemma nbhs_pinfty_gt r : r \is Num.real -> \forall x \near +oo, r < x.
-Proof. by exists r. Qed.
+Proof.
+move=> realr; exists (r + 1); split; first by rewrite realD.
+by move=> x; apply: lt_le_trans; rewrite ltr_addl.
+Qed.
 
 Lemma nbhs_pinfty_ge r : r \is Num.real -> \forall x \near +oo, r <= x.
-Proof. by exists r; split => //; apply: ltW. Qed.
+Proof. by exists r. Qed.
 
 Lemma nbhs_ninfty_lt r : r \is Num.real -> \forall x \near -oo, r > x.
-Proof. by exists r. Qed.
+Proof.
+move=> r0; exists (r - 1); split; first by rewrite realB//.
+by move=> x /le_lt_trans; apply; rewrite ltr_subl_addl ltr_addr.
+Qed.
 
 Lemma nbhs_ninfty_le r : r \is Num.real -> \forall x \near -oo, r >= x.
-Proof. by exists r; split => // ?; apply: ltW. Qed.
+Proof. by exists r. Qed.
 
 Lemma nbhs_pinfty_real : \forall x \near +oo, x \is @Num.real R.
 Proof. by apply: filterS (nbhs_pinfty_gt (@real0 _)); apply: gtr0_real. Qed.
@@ -519,8 +525,9 @@ Proof. exact: pinfty_ex_gt. Qed.
 Lemma near_pinfty_div2 (A : set R) :
   (\forall k \near +oo, A k) -> (\forall k \near +oo, A (k / 2)).
 Proof.
-move=> [M [Mreal AM]]; exists (M * 2); split; first by rewrite realM.
-by move=> x; rewrite -ltr_pdivl_mulr //; exact: AM.
+move=> [M [Mreal AM]]; exists (M * 2); split.
+  by rewrite realM // realE; apply/orP; left.
+by move=> x; rewrite -ler_pdivl_mulr //; apply: AM.
 Qed.
 
 End infty_nbhs_instances.
@@ -567,7 +574,7 @@ tfae; first by move=> Foo A Areal; apply: Foo; apply: nbhs_pinfty_ge.
 - by move=> Foo; near do apply: Foo => //.
 - by apply: filterS => ?; apply: filterS => ?; apply: ltW.
 case=> [A [AR AF]] P [x [xR Px]]; near +oo_R => B.
-by near do [apply: Px; apply: (@lt_le_trans _ _ B) => //]; apply: AF.
+by near do [apply: Px; apply: (@le_trans _ _ B) => //]; apply: AF.
 Unshelve. all: by end_near. Qed.
 
 Let cvgrNyPnum {F : set (set R)} {FF : Filter F} : [<->
@@ -583,7 +590,7 @@ tfae; first by move=> Foo A Areal; apply: Foo; apply: nbhs_ninfty_le.
 - by move=> Foo; near do apply: Foo => //.
 - by apply: filterS => ?; apply: filterS => ?; apply: ltW.
 case=> [A [AR AF]] P [x [xR Px]]; near -oo_R => B.
-by near do [apply: Px; apply: (@le_lt_trans _ _ B) => //]; apply: AF.
+by near do [apply: Px; apply: (@le_trans _ _ B) => //]; apply: AF.
 Unshelve. all: end_near. Qed.
 
 Context {T} {F : set (set T)} {FF : Filter F}.
@@ -714,7 +721,7 @@ tfae; first by move=> Foo A Areal; apply: Foo; apply: ereal_nbhs_pinfty_ge.
 - by move=> Foo; near do apply: Foo => //.
 - by apply: filterS => ?; apply: filterS => ?; apply: ltW.
 case=> [A [AR AF]] P [x [xR Px]]; near +oo_R => B.
-by near do [apply: Px; rewrite (@lt_le_trans _ _ B%:E) ?lte_fin//]; apply: AF.
+by near do [apply: Px; rewrite (@le_trans _ _ B%:E) ?lee_fin//]; apply: AF.
 Unshelve. all: end_near. Qed.
 
 Let cvgeNyPnum {F : set (set \bar R)} {FF : Filter F} : [<->
@@ -730,7 +737,7 @@ tfae; first by move=> Foo A Areal; apply: Foo; apply: ereal_nbhs_ninfty_le.
 - by move=> Foo; near do apply: Foo => //.
 - by apply: filterS => ?; apply: filterS => ?; apply: ltW.
 case=> [A [AR AF]] P [x [xR Px]]; near -oo_R => B.
-by near do [apply: Px; rewrite (@le_lt_trans _ _ B%:E) ?lte_fin//]; apply: AF.
+by near do [apply: Px; rewrite (@le_trans _ _ B%:E) ?lee_fin//]; apply: AF.
 Unshelve. all: end_near. Qed.
 
 Context {T} {F : set (set T)} {FF : Filter F}.
@@ -2518,7 +2525,7 @@ Lemma bounded_fun_has_ubound (T : Type) (R : realFieldType) (a : T -> R) :
   bounded_fun a -> has_ubound (range a).
 Proof.
 move=> [M [Mreal]]/(_ (`|M| + 1)).
-rewrite (le_lt_trans (ler_norm _)) ?ltr_addl// => /(_ erefl) aM.
+rewrite (le_trans (ler_norm _)) ?ler_addl// => /(_ erefl) aM.
 by exists (`|M| + 1) => _ [n _ <-]; rewrite (le_trans (ler_norm _))// aM.
 Qed.
 
@@ -2542,8 +2549,8 @@ Proof.
 move=> [M [Mreal Ma]] [N [Nreal Nb]].
 rewrite /bounded_fun/bounded_near; near=> x => y /= _.
 rewrite (le_trans (ler_norm_add _ _))// [x]splitr.
-by rewrite ler_add// (Ma, Nb)// ltr_pdivl_mulr//;
-   near: x; apply: nbhs_pinfty_gt; rewrite ?rpredM ?rpred_nat.
+by rewrite ler_add// (Ma, Nb)// ler_pdivl_mulr//;
+  near: x; apply: nbhs_pinfty_ge; rewrite ?rpredM ?rpred_nat.
 Unshelve. all: by end_near. Qed.
 
 Lemma bounded_locally (T : topologicalType)
@@ -3588,9 +3595,9 @@ Lemma abse_continuous : continuous (@abse R).
 Proof.
 case=> [r|A /= [r [rreal rA]]|A /= [r [rreal rA]]]/=.
 - exact/(cvg_comp (@norm_continuous _ [normedModType R of R^o] r)).
-- by exists r; split => // y ry; apply: rA; rewrite (lt_le_trans ry)// lee_abs.
-- exists (- r)%R; rewrite realN; split => // y; rewrite EFinN -lte_oppr => yr.
-  by apply: rA; rewrite (lt_le_trans yr)// -abseN lee_abs.
+- by exists r; split => // y ry; apply: rA; rewrite (le_trans ry)// lee_abs.
+- exists (- r)%R; rewrite realN; split => // y; rewrite EFinN -lee_oppr => yr.
+  by apply: rA; rewrite (le_trans yr)// -abseN lee_abs.
 Qed.
 
 Lemma cvg_abse f (a : \bar R) : f @ F --> a -> `|f x|%E @[x --> F] --> `|a|%E.
@@ -3624,10 +3631,10 @@ move=> [s||]/=.
   by apply: near_fun => //=; apply: continuousM => //=; apply: cvg_cst.
 - rewrite muleC /mule/= eqe gt_eqF// lte_fin r0 => A [u [realu uA]].
   exists (r^-1 * u)%R; split; first by rewrite realM// realV realE ltW.
-  by move=> x rux; apply: uA; move: rux; rewrite EFinM lte_pdivr_mull.
+  by move=> x rux; apply: uA; move: rux; rewrite EFinM lee_pdivr_mull.
 - rewrite muleC /mule/= eqe gt_eqF// lte_fin r0 => A [u [realu uA]].
   exists (r^-1 * u)%R; split; first by rewrite realM// realV realE ltW.
-  by move=> x xru; apply: uA; move: xru; rewrite EFinM lte_pdivl_mull.
+  by move=> x xru; apply: uA; move: xru; rewrite EFinM lee_pdivl_mull.
 Unshelve. all: by end_near. Qed.
 
 Lemma cvgeMl f x y : y \is a fin_num ->
@@ -4512,43 +4519,54 @@ case: x => [x|//|] xy; first exact: open_ereal_lt.
 - case: y => [y||//] /= in xy *; last by exists 0%R.
   by exists y; rewrite num_real; split => //= x ?.
 - case: y => [y||//] /= in xy *.
-  + by exists y; rewrite num_real; split => //= x ?.
-  + by exists 0%R; split => // x /lt_le_trans; apply; rewrite leey.
+  + exists (y - 1)%R; rewrite num_real; split => //= x /le_lt_trans; apply.
+    by rewrite lte_fin ltr_subl_addr ltr_addl.
+  + by exists 0%R; split => // x /le_lt_trans; apply.
 Qed.
 
 Lemma open_ereal_gt' x y : y < x -> ereal_nbhs x (fun u => y < u).
 Proof.
 case: x => [x||] //=; do ?[exact: open_ereal_gt];
   case: y => [y||] //=; do ?by exists 0.
-- by exists y; rewrite num_real.
-- by move=> _; exists 0%R; split => // x; apply/le_lt_trans; rewrite leNye.
+- exists (y + 1)%R; rewrite num_real; split => // x /lt_le_trans; apply.
+  by rewrite lte_fin ltr_addl.
+- by move=> _; exists 0%R; split => // x; exact/lt_le_trans.
 Qed.
 
-Lemma open_ereal_lt_ereal x : open [set y | y < x].
+Let open_ereal_lt_real r : open (fun x => x < r%:E).
 Proof.
-have openr r : open [set x | x < r%:E].
-  case => [? | // | ?]; [rewrite /= lte_fin => xy | by exists r].
+case => [? | // | ?]; [rewrite lte_fin => xy | exists (r - 1)%R].
   by move: (@open_ereal_lt r%:E); rewrite openE; apply; rewrite /= lte_fin.
-case: x => [ // | | [] // ].
+rewrite num_real; split => // x /le_lt_trans; apply.
+by rewrite lte_fin ltr_subl_addr ltr_addl.
+Qed.
+
+Lemma open_ereal_lt_ereal x : open [set y | y < x].
+Proof.
+case: x => [x | | [] // ] /=; first exact: open_ereal_lt_real.
 suff -> : [set y | y < +oo] = \bigcup_r [set y : \bar R | y < r%:E].
-  exact: bigcup_open.
+  by apply bigcup_open => x _; exact: open_ereal_lt_real.
 rewrite predeqE => -[r | | ]/=.
-- rewrite ltry; split => // _.
+- rewrite ltey; split => // _.
   by exists (r + 1)%R => //=; rewrite lte_fin ltr_addl.
 - by rewrite ltxx; split => // -[] x /=; rewrite ltNge leey.
 - by split => // _; exists 0%R => //=.
 Qed.
 
-Lemma open_ereal_gt_ereal x : open [set y | x < y].
+Let open_ereal_gt_real r : open (fun x => r%:E < x).
 Proof.
-have openr r : open [set x | r%:E < x].
-  case => [? | ? | //]; [rewrite /= lte_fin => xy | by exists r].
+case => [? | ? | //]; [rewrite lte_fin => xy | exists (r + 1)%R].
   by move: (@open_ereal_gt r%:E); rewrite openE; apply; rewrite /= lte_fin.
-case: x => [ // | [] // | ].
+by rewrite num_real; split=> // x /lt_le_trans; apply; rewrite lte_fin ltr_addl.
+Qed.
+
+Lemma open_ereal_gt_ereal x : open [set y | x < y].
+Proof.
+case: x => [x | [] // | ] /=; first exact: open_ereal_gt_real.
 suff -> : [set y | -oo < y] = \bigcup_r [set y : \bar R | r%:E < y].
-  exact: bigcup_open.
+  by apply bigcup_open => x _; exact: open_ereal_gt_real.
 rewrite predeqE => -[r | | ]/=.
-- rewrite ltNyr; split => // _.
+- rewrite ltNye; split => // _.
   by exists (r - 1)%R => //=; rewrite lte_fin ltr_subl_addr ltr_addl.
 - by split => // _; exists 0%R => //=.
 - by rewrite ltxx; split => // -[] x _ /=; rewrite ltNge leNye.
@@ -5702,8 +5720,8 @@ have /Aco [] := covA.
 move=> D _ DcovA.
 exists (\big[maxr/0]_(i : D) (fsval i)%:~R).
 rewrite bigmax_real//; last by move=> ? _; rewrite realz.
-split => // x ltmaxx p /DcovA [n Dn /lt_trans /(_ _)/ltW].
-apply; apply: le_lt_trans ltmaxx.
+split => // x ltmaxx p /DcovA [n Dn /lt_le_trans /(_ _)/ltW].
+apply; apply: le_trans ltmaxx.
 have : n \in enum_fset D by [].
 by rewrite enum_fsetE => /mapP[/= i iD ->]; exact/le_bigmax.
 Qed.
@@ -5775,13 +5793,12 @@ have Mnco : compact
   by move=> _; apply: segment_compact.
 apply: subclosed_compact Acl Mnco _ => v /normAltM normvleM i.
 suff : `|v ord0 i : R| <= M + 1 by rewrite ler_norml.
-apply: le_trans (normvleM _ _); last by rewrite ltr_addl.
+apply: le_trans (normvleM _ _); last by rewrite ler_addl.
 have /mapP[j Hj ->] : `|v ord0 i| \in [seq `|v x.1 x.2| | x : 'I_1 * 'I_n.+1].
   by apply/mapP; exists (ord0, i) => //=; rewrite mem_enum.
 by rewrite [leRHS]/normr /= mx_normrE; apply/bigmax_geP; right => /=; exists j.
 Qed.
 
-
 (** * Some limits on real functions *)
 
 Section Shift.
@@ -6203,7 +6220,7 @@ split => [/(_ 1) [M Bf]|/linear_boundedP fr y].
   by rewrite sub0r normrN => x1; exact/Bf/ltW.
 near +oo_R => r; exists (r * y) => x xe.
 rewrite (@le_trans _ _ (r * `|x|)) //; first by move: {xe} x; near: r.
-by rewrite ler_pmul //.
+by rewrite ler_pmul.
 Unshelve. all: by end_near. Qed.
 
 End LinearContinuousBounded.
diff --git a/theories/realfun.v b/theories/realfun.v
index b84a816cc0..e0a54c6114 100644
--- a/theories/realfun.v
+++ b/theories/realfun.v
@@ -52,7 +52,7 @@ Lemma cvg_addrl (M : R) : M + r @[r --> +oo] --> +oo.
 Proof.
 move=> P [r [rreal rP]]; exists (r - M); split.
   by rewrite realB// num_real.
-by move=> m; rewrite ltr_subl_addl => /rP.
+by move=> m; rewrite ler_subl_addl => /rP.
 Qed.
 
 (* NB: see cvg_addnr in topology.v *)
@@ -161,7 +161,7 @@ have [Spoo|Spoo] := pselect (S +oo).
   have -> : l = +oo by rewrite /l /ereal_sup; exact: supremum_pinfty.
   rewrite -(cvg_shiftr `|N|); apply: cvg_near_cst.
   exists N; split; first by rewrite num_real.
-  by move=> x /ltW Nx; rewrite Nf// ler_paddr.
+  by move=> x Nx; rewrite Nf// ler_paddr.
 have [lpoo|lpoo] := eqVneq l +oo.
   rewrite lpoo; apply/cvgeyPge => M.
   have /ereal_sup_gt[_ [n _] <- Mun] : M%:E < l by rewrite lpoo// ltry.
@@ -188,7 +188,7 @@ have xB r : (x <= r)%R -> B r.
   by move: xr; rewrite urnoo leeNy_eq; exact/negP.
 rewrite -(@fineK _ l)//; apply/fine_cvgP; split.
   exists x; split; first by rewrite num_real.
-  by move=> r A1r; rewrite f_fin_num //; exact/xB/ltW.
+  by move=> r A1r; rewrite f_fin_num //; exact/xB.
 set g := fun n => if (n < x)%R then fine (f x) else fine (f n).
 have <- : sup (range g) = fine l.
   apply: EFin_inj; rewrite -ereal_sup_EFin//; last 2 first.
diff --git a/theories/sequences.v b/theories/sequences.v
index 3ab4bc4754..268d7452b1 100644
--- a/theories/sequences.v
+++ b/theories/sequences.v
@@ -2115,7 +2115,7 @@ move=> cf; have [M [Mreal Mu]] := cvg_seq_bounded cf.
 apply: nonincreasing_is_cvgn.
   exact/nonincreasing_sups/bounded_fun_has_ubound/cvg_seq_bounded.
 exists (- (M + 1)) => _ [n _ <-]; rewrite (@le_trans _ _ (u n)) //.
-  by apply/lerNnormlW/Mu => //; rewrite ltr_addl.
+  by apply/lerNnormlW/Mu => //; rewrite ler_addl.
 apply: sup_ub; last by exists n => /=.
 exact/has_ubound_sdrop/bounded_fun_has_ubound/cvg_seq_bounded.
 Qed.
diff --git a/theories/topology.v b/theories/topology.v
index 5d493bd14f..7d54ae23e6 100644
--- a/theories/topology.v
+++ b/theories/topology.v
@@ -652,7 +652,7 @@ Local Notation "{ 'all3' P }" := (forall x y z, P x y z: Prop) (at level 0).
 Local Notation ph := (phantom _).
 
 Definition prop_near1 {X} {fX : filteredType X} (x : fX)
-   P (phP : ph {all1 P}) := nbhs x P.
+  P (phP : ph {all1 P}) := nbhs x P.
 
 Definition prop_near2 {X X'} {fX : filteredType X} {fX' : filteredType X'}
   (x : fX) (x' : fX') := fun P of ph {all2 P} =>
@@ -705,7 +705,7 @@ Arguments cvg_refl {T F}.
 #[global] Hint Resolve cvg_refl : core.
 
 Lemma cvg_trans T (G F H : set (set T)) :
-  (F `=>` G) -> (G `=>` H) -> (F `=>` H).
+  F `=>` G -> G `=>` H -> F `=>` H.
 Proof. by move=> FG GH P /GH /FG. Qed.
 
 Notation "F --> G" := (cvg_to [filter of F] [filter of G]) : classical_set_scope.