diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index c1ee5bdc8..1e029fa12 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -6,6 +6,15 @@
 
 ### Changed
 
+- in `ereal.v`:
+  + lemmas `lee_paddl`, `lte_addl`, `lee_paddr`, `lte_paddr`, `lee_lt_add`
+- 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
 
 ### Removed
diff --git a/theories/derive.v b/theories/derive.v
index eeedb6157..cee86a4fd 100644
--- a/theories/derive.v
+++ b/theories/derive.v
@@ -171,7 +171,7 @@ move=> /diff_locallyP [dfc]; rewrite -addrA.
 rewrite (littleo_bigO_eqo (cst (1 : R))); last first.
   apply/eqOP; near=> k; rewrite /cst [`|1|]normr1 mulr1.
   near=> y; rewrite ltW //; near: y; apply/nbhs_normP.
-  exists k; first by near: k; exists 0.
+  exists k => /=; first by near: k; exact: nbhs_pinfty_gt.
   by move=> ? /=; rewrite -ball_normE /= sub0r normrN.
 rewrite addfo; first by move=> /eqolim; rewrite cvg_comp_shift add0r.
 by apply/eqolim0P; apply: (cvg_trans (dfc 0)); rewrite linear0.
@@ -1307,8 +1307,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 f86e967d7..798844a80 100644
--- a/theories/ereal.v
+++ b/theories/ereal.v
@@ -1588,6 +1588,10 @@ move: x y a b => [x| |] [y| |] [a| |] [b| |] _ _ //=; rewrite ?(ltey, ltNye)//.
 by rewrite !lte_fin; exact: ltr_le_add.
 Qed.
 
+Lemma lee_lt_add a b x y : a \is a fin_num -> b \is a fin_num ->
+  a <= x -> b < y -> a + b < x + y.
+Proof. by move=> afin bin xa yb; rewrite (addeC a) (addeC x) lte_le_add. Qed.
+
 Lemma lee_sub x y z u : x <= y -> u <= z -> x - z <= y - u.
 Proof.
 move: x y z u => -[x| |] -[y| |] -[z| |] -[u| |] //=; rewrite ?(leey,leNye)//.
@@ -2648,6 +2652,18 @@ exists (PosNum xy); apply/negP; rewrite -ltNge lte_fin -ltr_subr_addl.
 by rewrite ltr_pdivr_mulr // ltr_pmulr ?subr_gt0 // ltr1n.
 Qed.
 
+Lemma lee_paddl y x z : 0 <= x -> y <= z -> y <= x + z.
+Proof. by move=> *; rewrite -[y]add0e lee_add. Qed.
+
+Lemma lte_paddl y x z : 0 <= x -> y < z -> y < x + z.
+Proof. by move=> x0 /lt_le_trans; apply; rewrite lee_paddl. Qed.
+
+Lemma lee_paddr y x z : 0 <= x -> y <= z -> y <= z + x.
+Proof. by move=> *; rewrite addeC lee_paddl. Qed.
+
+Lemma lte_paddr y x z : 0 <= x -> y < z -> y < z + x.
+Proof. by move=> *; rewrite addeC lte_paddl. Qed.
+
 Lemma lte_spaddr z x y : z \is a fin_num -> 0 < y -> z <= x -> z < x + y.
 Proof.
 move: z y x => [z| |] [y| |] [x| |] _ //=; rewrite ?(lte_fin, lte_fin, ltey) //.
@@ -3365,17 +3381,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.
 
 Lemma ereal_nbhs_pinfty_ge (R : numFieldType) (e : {posnum R}) :
@@ -3394,70 +3413,52 @@ 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]]|]; first 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.
 
@@ -3492,32 +3493,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) :=
@@ -3545,19 +3548,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)) :
@@ -3920,12 +3923,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 ->
@@ -4188,12 +4194,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.
@@ -4208,12 +4214,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.
@@ -4310,14 +4316,14 @@ 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.
-    apply; apply: lt_le_trans (lt_succ_Rfloor _) _; rewrite RfloorE Nfloor.
+    have /le_trans : (d <= Num.max d 0)%R by rewrite le_maxr lexx.
+    apply; apply: le_trans (ltW (lt_succ_Rfloor _)) _; rewrite RfloorE Nfloor.
     by rewrite -(@natrD R N 1) ler_nat addn1.
   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.
-  apply; apply: lt_le_trans (lt_succ_Rfloor _) _; rewrite RfloorE Nfloor.
+  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_Rfloor _)) _; rewrite RfloorE Nfloor.
   by rewrite -(@natrD R N 1) ler_nat addn1.
 have /ZnatP [N Nfloor] : floor (d%:num^-1) \is a Znat.
   by rewrite Znat_def floor_ge0.
diff --git a/theories/exp.v b/theories/exp.v
index 0731429b4..bde4d0bd7 100644
--- a/theories/exp.v
+++ b/theories/exp.v
@@ -56,7 +56,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 ccf86f3f0..2b04f8afc 100644
--- a/theories/landau.v
+++ b/theories/landau.v
@@ -474,8 +474,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.
 
@@ -500,8 +500,8 @@ Notation "[bigO 'of' f ]" := (@bigO_clone _ _ f _ _ idfun).
 
 Lemma bigO0_subproof F (g : T -> W) : Filter F -> bigO_def F (0 : T -> V) g.
 Proof.
-move=> FF; near=> k; apply: filterE => x; rewrite normr0 pmulr_rge0 ?normr_ge0//.
-by near: k; exists 0.
+move=> FF; near=> k; apply: filterE => x; rewrite normr0 pmulr_rge0//.
+by near: k; exact: nbhs_pinfty_gt.
 Unshelve. all: by end_near. Qed.
 
 Canonical bigO0 (F : filter_on T) g := BigO (asboolT (@bigO0_subproof F g _)).
@@ -673,9 +673,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 *)
@@ -1108,25 +1110,26 @@ 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 -ball_normE /= 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].
   by rewrite normr_le0 => /eqP->; rewrite linear0 !normr0 mulr0.
 have ky0 : 0 <= k0%:num / (k * `|y|).
-  by rewrite pmulr_rge0 // invr_ge0 mulr_ge0 // ltW //; near: k; exists 0.
-rewrite -[leRHS]mulr1 -ler_pdivr_mull ?pmulr_rgt0 //; last first.
-  by near: k; exists 0.
+  rewrite pmulr_rge0// invr_ge0 mulr_ge0// ltW//.
+  by near: k; exact: nbhs_pinfty_gt.
+rewrite -[X in _ <= X]mulr1 -ler_pdivr_mull ?pmulr_rgt0//; last first.
+  by near: k; exact: nbhs_pinfty_gt.
 rewrite -(ler_pmul2l [gt0 of k0%:num]) mulr1 mulrA -[_ / _]ger0_norm //.
 rewrite -normm_s.
 have <- : GRing.Scale.op s_law =2 s by rewrite GRing.Scale.opE.
 rewrite -linearZ fk //= -ball_normE /= distrC subr0 normmZ ger0_norm //.
 rewrite invfM mulrA mulfVK ?lt0r_neq0 // ltr_pdivr_mulr //; last first.
-  by near: k; exists 0.
-by rewrite -ltr_pdivr_mull//; near: k; exact: nbhs_pinfty_gt.
+  by near: k; exact: nbhs_pinfty_gt.
+by rewrite mulrC -ltr_pdivr_mulr //; near: k; exact: nbhs_pinfty_gt.
 Unshelve. all: by end_near. Qed.
 
 End Linear3.
@@ -1319,7 +1322,8 @@ Lemma addOmega (R : realFieldType) (F : filter_on pT) (f g h : _ -> R^o)
 Proof.
 rewrite 2!eqOmegaE !eqOmegaO => /eqOP hOf; apply/eqOP.
 apply: filter_app hOf; near=> k; apply: filter_app; near=> x => /le_trans.
-apply; rewrite ler_pmul2l //; last by near: k; exists 0.
+apply; rewrite ler_pmul2l //; last first.
+  by near: k; exists 1; split => // r; exact: lt_le_trans.
 by rewrite !ger0_norm // ?addr_ge0 // ler_addl.
 Unshelve. all: by end_near. Qed.
 
@@ -1333,7 +1337,9 @@ 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 //; near: k; exists (k2%:num * k1%:num)^-1.
+rewrite ler_wpmul2r// ltW//; near: k; exists ((k2%:num * k1%:num)^-1 + 1).
+rewrite realD// ?realV ?realM ?num_real; split => // x.
+by apply: lt_le_trans; rewrite ltr_addl.
 Unshelve. all: by end_near. Qed.
 
 End big_omega_in_R.
@@ -1495,7 +1501,9 @@ 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 //; near: k; exists (k2%:num * k1%:num)^-1.
+rewrite ler_wpmul2r // ltW //; near: k; exists ((k2%:num * k1%:num)^-1 +1).
+rewrite realD// ?realV ?realM ?num_real; split => // x.
+by apply: lt_le_trans; rewrite ltr_addl.
 Unshelve. all: by end_near. Qed.
 
 End big_theta_in_R.
diff --git a/theories/normedtype.v b/theories/normedtype.v
index 1d5d1c078..3bad38262 100644
--- a/theories/normedtype.v
+++ b/theories/normedtype.v
@@ -364,10 +364,10 @@ Proof. exact: Proper_dnbhs_numFieldType. 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" := (pinfty_nbhs _) : ring_scope.
@@ -381,11 +381,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 (Num.max 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.
 
@@ -393,32 +393,39 @@ 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 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.
 
 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.
 
 End infty_nbhs_instances.
 
@@ -1311,8 +1318,9 @@ Qed.
 Lemma pinfty_ex_gt {R : numFieldType} (m : R) (A : set R) : m \is Num.real ->
   (\forall k \near +oo, A k) -> exists2 M, m < M & A M.
 Proof.
-by move=> m_real Agt; near (pinfty_nbhs R) => M;
-   exists M; near: M => //; exists m.
+move=> m_real Agt; near (pinfty_nbhs R) => M;
+   exists M; near: M => //; exists (m + 1).
+by rewrite realD//; split=> // x; apply: lt_le_trans; rewrite ltr_addl.
 Unshelve. all: by end_near. Qed.
 
 Lemma pinfty_ex_gt0 {R : numFieldType} (A : set R) :
@@ -1443,7 +1451,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.
 
@@ -1451,7 +1459,7 @@ Lemma bounded_funN (T : Type) (R : realFieldType) (a : T -> R) :
   bounded_fun a -> bounded_fun (- a).
 Proof.
 move=> [M [Mreal aM]]; rewrite /bounded_fun /bounded_near; near=> x => y /= _.
-by rewrite normrN; apply: aM => //; near: x; apply: nbhs_pinfty_gt.
+by rewrite normrN; apply: aM => //; near: x; apply: nbhs_pinfty_ge.
 Unshelve. all: by end_near. Qed.
 
 Lemma bounded_fun_has_lbound (T : Type) (R : realFieldType) (a : T -> R) :
@@ -1467,8 +1475,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)
@@ -1620,10 +1628,9 @@ Lemma cvg_bounded_real {F : set (set V)} {FF : Filter F} (y : V) :
   F --> y ->
   \forall M \near +oo, \forall y' \near F, `|y'| < M.
 Proof.
-move=> /cvg_dist Fy; exists `|y|; rewrite normr_real; split => // M.
-rewrite -subr_gt0 => subM_gt0.
-have := Fy _ subM_gt0.
-apply: filterS => y' yy'; rewrite -(@ltr_add2r _ (- `|y|)).
+move=> /cvg_dist Fy; exists (`|y| + 1); rewrite realD//; split => // M.
+rewrite -ler_subr_addl => /(ltr_spaddl ltr01); rewrite -ltr_subl_addl subrr.
+move/Fy; apply: filterS => y' yy'; rewrite -(@ltr_add2r _ (- `|y|)).
 rewrite (le_lt_trans _ yy') // (le_trans _ (ler_dist_dist _ _)) // distrC.
 by rewrite real_ler_norm.
 Qed.
@@ -1631,8 +1638,10 @@ Qed.
 Lemma cvg_bounded {F : set (set V)} {FF : Filter F} (y : V) :
   F --> y -> bounded_near id F.
 Proof.
-move=> /cvg_dist Fy; exists `|y|; rewrite normr_real; split => //= M.
-rewrite -subr_gt0 => /Fy; apply: filterS => y' yy'; apply: ltW.
+move=> /cvg_dist Fy; exists (`|y| + 1); rewrite realD//; split => //= M.
+rewrite -ler_subr_addl => /(ltr_spaddl ltr01).
+rewrite -ltr_subl_addl subrr.
+move=> /Fy; apply: filterS => y' yy'; apply: ltW.
 by rewrite -(@ltr_add2r _ (- `|y|)) (le_lt_trans (ler_sub_dist _ _))// distrC.
 Qed.
 
@@ -2123,11 +2132,11 @@ move=> [x| |] /=.
     by rewrite EFinM.
   exact: (cvg_comp (@scaler_continuous _ _ _ _)).
 - rewrite muleC /mule/= eqe gt_eqF// lte_fin r0 => A [u [realu uA]].
-  exists (r^-1 * u); split; first by rewrite realM// realV realE ltW.
-  by move=> x rux; apply uA; move: rux; rewrite EFinM lte_pdivr_mull.
+  exists (r^-1 * u); split; first by rewrite realM// realV// realE (ltW r0).
+  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); split; first by rewrite realM// realV realE ltW.
-  by move=> x xru; apply uA; move: xru; rewrite EFinM lte_pdivl_mull.
+  exists (r^-1 * u); split; first by rewrite realM// realV// realE (ltW r0).
+  by move=> x xru; apply uA; move: xru; rewrite EFinM lee_pdivl_mull.
 Unshelve. all: by end_near. Qed.
 
 End mule_continuous.
@@ -2136,9 +2145,9 @@ Lemma abse_continuous (R : realFieldType) : 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 (T : topologicalType) (R : realFieldType) (F : set (set T)) f
@@ -3404,8 +3413,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/ler_bigmax.
 Qed.
@@ -3477,7 +3486,7 @@ 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_gerP; right => /=; exists j.
@@ -3513,22 +3522,26 @@ 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.
 
 Let open_ereal_lt_real r : open (fun x => x < r%:E).
 Proof.
-case => [? | // | ?]; [rewrite lte_fin => xy | by exists r].
-by move: (@open_ereal_lt r%:E); rewrite openE; apply; rewrite /= lte_fin.
+case => [? | // | ?]; [rewrite lte_fin => xy | exists (r - 1)%R].
+  by move: (@open_ereal_lt r%:E); rewrite openE; apply; rewrite /= lte_fin.
+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].
@@ -3545,8 +3558,9 @@ Qed.
 
 Let open_ereal_gt_real r : open (fun x => r%:E < x).
 Proof.
-case => [? | ? | //]; [rewrite lte_fin => xy | by exists r].
-by move: (@open_ereal_gt r%:E); rewrite openE; apply; rewrite /= lte_fin.
+case => [? | ? | //]; [rewrite lte_fin => xy | exists (r + 1)%R].
+  by move: (@open_ereal_gt r%:E); rewrite openE; apply; rewrite /= lte_fin.
+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].
@@ -4029,31 +4043,33 @@ Proof.
 move=> /cvg_ballP/(_ _ ltr01); rewrite linear0 nearE => /nbhs_ex[e ef1].
 apply/linear_boundedP; near=> d; move=> x.
 have [->|x0] := eqVneq x 0; first by rewrite linear0 !normr0 mulr0.
-have d0 : 0 < d by near: d; exists 1; split => // r; apply le_lt_trans.
+have d0 : 0 < d by near: d; exact: nbhs_pinfty_gt.
 pose dx := d * `|x|; have dx0 : 0 < dx by rewrite mulr_gt0 // normr_gt0.
-suff : `| f (dx^-1 *: x) | < 1.
+suff : `| f (dx^-1 *: x) | <= 1.
   rewrite linearZ normmZ normfV ?gt_eqF //.
-  by rewrite ltr_pdivr_mull ?(normr_gt0,gt_eqF)// mulr1 gtr0_norm// => /ltW.
-suff /ef1 : ball 0 e%:num (dx^-1 *: x) by rewrite -ball_normE /= sub0r normrN.
+  by rewrite ler_pdivr_mull ?(normr_gt0,gt_eqF)// mulr1 gtr0_norm.
+suff /ef1 : ball 0 e%:num (dx^-1 *: x).
+  by rewrite -ball_normE /= sub0r normrN => /ltW.
 rewrite -ball_normE /ball_ /= sub0r normrN normmZ normfV ?gt_eqF //.
 rewrite normrM normr_id (gtr0_norm d0) invfM ?(normr_eq0,gt_eqF)//.
 rewrite mulrAC -mulrA mulfV ?normr_eq0 // mulr1 -div1r ltr_pdivr_mulr //.
-by near: d; exists e%:num^-1; split=> // r; rewrite -ltr_pdivr_mull ?mulr1.
+near: d; exists (e%:num^-1 + 1).
+rewrite realD ?realV// ?realE ?posnum_ge0; split => // r.
+by rewrite -ltr_pdivr_mull ?mulr1//; apply: lt_le_trans; rewrite ltr_addl.
 Unshelve. all: by end_near. Qed.
 
 Lemma linear_bounded0 (f : {linear V -> W}) :
   bounded_near f (nbhs (0 : V)) -> {for 0, continuous f}.
 Proof.
 move=> /linear_boundedP [y [yreal fr]]; near (@pinfty_nbhs R) => r.
-have r0  : 0 < r by near: r; exists 1; split => // z; apply le_lt_trans.
+have r0  : 0 < r by near: r; exact: nbhs_pinfty_gt.
 apply/cvg_ballP => _/posnumP[e]; rewrite nearE linear0 /= nbhs_ballP.
 exists (e%:num / 2 / r); first by rewrite /= divr_gt0.
 move=> x; rewrite -2!ball_normE /= 2!sub0r 2!normrN => xer.
 rewrite (@le_lt_trans _ _ (e%:num / 2)) //; last first.
   by rewrite gtr_pmulr // invf_lt1 // ltr1n.
 move: xer; rewrite ltr_pdivl_mulr // => /ltW; apply le_trans.
-rewrite mulrC; apply fr; near: r; exists (y + 1) => //.
-by rewrite realD//; split => // z; apply le_lt_trans; rewrite ler_addl.
+by rewrite mulrC; apply fr; near: r; exists y.
 Unshelve. all: by end_near. Qed.
 
 Lemma continuousfor0_continuous (f : {linear V -> W}) :
@@ -4061,14 +4077,12 @@ Lemma continuousfor0_continuous (f : {linear V -> W}) :
 Proof.
 move=> /linear_continuous0 /linear_boundedP [y [yreal fr]].
 near (@pinfty_nbhs R) => r.
-have r0  : 0 < r by near: r; exists 1; split => // z; apply le_lt_trans.
+have r0 : 0 < r by near: r; exact: nbhs_pinfty_gt.
 move=> x; apply/cvg_ballP => _/posnumP[e]; rewrite nearE /= nbhs_ballP.
 exists (e%:num / r); first by rewrite /= divr_gt0.
 move=> z; rewrite -!ball_normE //= => xy; rewrite -linearB.
 move: xy; rewrite ltr_pdivl_mulr //; apply le_lt_trans.
-rewrite mulrC; apply fr.
-near: r; exists (y + 1); rewrite realD //; split => // x.
-by apply le_lt_trans; rewrite ler_addl.
+by rewrite mulrC; apply fr; near: r; exists y.
 Unshelve. all: by end_near. Qed.
 
 Lemma linear_bounded_continuous (f : {linear V -> W}) :
@@ -4087,7 +4101,7 @@ split => [/(_ 1) [M Bf]|/linear_boundedP fr y].
   by rewrite -ball_normE /ball_ /= sub0r normrN => x1; exact/Bf/ltW.
 near (@pinfty_nbhs R) => r; exists (y * r) => x xe.
 rewrite mulrC (@le_trans _ _ (r * `|x|)) //; first by move: {xe} x; near: r.
-by rewrite ler_pmul //; near: r; exists 1; split => // x /ltW; apply le_trans.
+by rewrite ler_pmul //; near: r; exact: nbhs_pinfty_ge.
 Unshelve. all: by end_near. Qed.
 
 End LinearContinuousBounded.
diff --git a/theories/sequences.v b/theories/sequences.v
index 161a69136..2600ce71d 100644
--- a/theories/sequences.v
+++ b/theories/sequences.v
@@ -391,8 +391,8 @@ split => [u_cvg A|u_ge X [A [Ar AX]]].
   rewrite -(near_map u_ \oo (<=%R A)).
   by apply: u_cvg; apply: nbhs_pinfty_ge; rewrite num_real.
 rewrite !near_simpl [\near u_, X _](near_map u_ \oo); near=> x.
-apply: AX; rewrite (@lt_le_trans _ _ ((maxr 0 A) +1)) //.
-  by rewrite ltr_spaddr // le_maxr lexx orbT.
+apply: AX; rewrite (@le_trans _ _ ((maxr 0 A) +1)) //.
+  by rewrite ler_paddr // le_maxr lexx orbT.
 by near: x; apply: u_ge; rewrite ltr_spaddr // le_maxr lexx.
 Unshelve. all: by end_near. Qed.
 
@@ -402,7 +402,7 @@ rewrite propeqE; split => u_cvg P [/= l [l_real Pl]];
 rewrite !near_simpl [\forall x \near _, P _](near_map _ \oo);
 have [|/=n _]:= u_cvg (fun x => P (- x)); do ?by [exists n
   | exists (- l); split; rewrite ?rpredN// => x;
-    rewrite (ltr_oppl, ltr_oppr); apply: Pl].
+    rewrite (ler_oppl, ler_oppr); apply: Pl].
 by under [X in _ `<=` X]funext do rewrite /= opprK; exists n.
 Qed.
 
@@ -1670,8 +1670,8 @@ split => [u_cvg _/posnumP[A]|u_ge X [A [Ar AX]]].
   by apply: u_cvg; apply: ereal_nbhs_pinfty_ge.
 rewrite !near_simpl [\near u_, X _](near_map u_ \oo); near=> x.
 apply: AX.
-rewrite (@lt_le_trans _ _ (maxr 0 A + 1)%:E) //.
-  by rewrite EFinD lte_spaddr // ?lte_fin// lee_fin le_maxr lexx orbT.
+rewrite (@le_trans _ _ (maxr 0 A + 1)%:E) //.
+  by rewrite EFinD lee_paddr// lee_fin// le_maxr lexx orbT.
 by near: x; apply: u_ge; rewrite ltr_spaddr // le_maxr lexx.
 Unshelve. all: by end_near. Qed.
 
@@ -1683,9 +1683,9 @@ split => [u_cvg A A0|u_le X [A [Ar AX]]].
   by apply: u_cvg; apply: ereal_nbhs_ninfty_le.
 rewrite !near_simpl [\near u_, X _](near_map u_ \oo); near=> x.
 apply: AX.
-rewrite (@le_lt_trans _ _ (minr 0 A - 1)%:E) //.
+rewrite (@le_trans _ _ (minr 0 A - 1)%:E) //.
   by near: x; apply: u_le; rewrite ltr_subl_addl addr0 lt_minl ltr01.
-by rewrite lte_fin ltr_subl_addl lt_minl ltr_addr ltr01 orbT.
+by rewrite lee_fin ler_subl_addl le_minl ler_addr ler01 orbT.
 Unshelve. all: by end_near. Qed.
 
 Lemma ereal_squeeze (R : realType) (f g h : (\bar R)^nat) :
@@ -2163,7 +2163,7 @@ move=> cf; have [M [Mreal Mu]] := cvg_seq_bounded cf.
 apply: nonincreasing_is_cvg.
   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 a73fa514d..e25190403 100644
--- a/theories/topology.v
+++ b/theories/topology.v
@@ -721,7 +721,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} =>
@@ -768,7 +768,7 @@ Proof. exact. Qed.
 #[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.