diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 4ee12401e3..242a56d718 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -21,18 +21,34 @@
   + lemmas `at_rightD`, `at_leftD`, `near_at_rightD`, `near_at_leftD`,
     `at_left_shift`, `at_right_shift`
 
+- in `num_normedtype.v`,
+  + lemmas `pinftyV`, `ninftyV`, `cvgryV`, `cvgrNyV`, `lt0_cvgMlNy`, 
+    `lt0_cvgMrNy`, `lt0_cvgMly`, `lt0_cvgMry`
+
+- in `pseudometric_normed_Zmodule.v`,
+  + lemmas `fmap_at_left0P`, `fmap_at_right0E`
+
+- in `tvs.v`,
+  + lemmas `near_shiftE`, `nearZE`
+
+- in `num_topology.v`:
+  + lemmas `near_right_in_itv`, `near_left_in_itv`
+
 ### Changed
 
 - in `derive.v`:
   + instance `is_derive_mx` is now a lemma
 
 - moved from `metric_structure.v` to `num_topology.v`: 
-  + lemma `cvg_at_right_left_dnbhs`, generalized to `topologicalType` from `metricType`.
+  + lemma `cvg_at_right_left_dnbhs`, generalized to `topologicalType` from `metricType`
 
 ### Renamed
 
 ### Generalized
 
+- in `tvs.v`:
+  + lemma `nbhsB`
+
 ### Deprecated
 
 ### Removed
diff --git a/theories/normedtype_theory/num_normedtype.v b/theories/normedtype_theory/num_normedtype.v
index 5ae913e592..6fc359f6cd 100644
--- a/theories/normedtype_theory/num_normedtype.v
+++ b/theories/normedtype_theory/num_normedtype.v
@@ -245,6 +245,53 @@ apply/seteqP; split => [A [M [Mreal MA]]|A [M [Mreal MA]]].
 by exists (- M); rewrite ?realN; split=> // x; rewrite ltrNl => /MA.
 Qed.
 
+Lemma pinftyV (R : numFieldType) : x^-1 @[x --> +oo] = (0 : R)^'+.
+Proof.
+apply/seteqP; split=> [A [M [Mreal MA]]|A [r /= r0 rA]].
+- have mM1_gt0 : 0 < Num.max M 1.
+    case: (@real_leP _ M 1) => //.
+    by apply: lt_trans.
+  exists (Num.max M 1)^-1; first by rewrite /= invr_gt0.
+  move=> x /= /[swap] x_gt0.
+  rewrite distrC subr0 gtr0_norm// invf_pgt ?posrE// => mM1_lt_xV.
+  rewrite -(invrK x); apply: MA.
+  apply: le_lt_trans mM1_lt_xV.
+  by case: (@real_leP _ M 1).
+- exists r^-1; split; first by rewrite realV gtr0_real.
+  move=> x /[dup] rV_lt_x.
+  have x_gt0 : x > 0.
+    apply: lt_trans rV_lt_x.
+    by rewrite invr_gt0.
+  rewrite invf_plt// => xV_lt_r.
+  apply: rA; last by rewrite invr_gt0.
+  by rewrite /= distrC subr0 gtr0_norm// invr_gt0.
+Qed.
+
+Lemma ninftyV (R : numFieldType) : x^-1 @[x --> -oo] = (0 : R)^'-.
+Proof.
+apply/seteqP; split=> [A [M [Mreal MA]]|A [r /= r0 rA]].
+- pose M' := Num.min M (-1).
+  have M'_lt0 : M' < 0.
+    rewrite /M'.
+    case: (@real_leP _ M (-1)) => // /le_lt_trans.
+    by apply.
+  exists (-M')^-1; first by rewrite /= invr_gt0 oppr_gt0.
+  move=> x /= /[swap] x_lt0.
+  rewrite distrC subr0 ltr0_norm// invrN ltrN2 => x_gt_VM'.
+  rewrite -(invrK x); apply: MA.
+  apply: (lt_le_trans (y := M')).
+  + by rewrite invf_nlt.
+  + by rewrite /M'; case: (@real_ltP _ M (-1)).
+- exists (- r^-1); split; first by rewrite realN realV gtr0_real.
+  move=> x /[dup] x_lt_NrV.
+  have x_lt0 : x < 0.
+    apply: (lt_trans x_lt_NrV).
+    by rewrite oppr_lt0 invr_gt0.
+  rewrite ltrNr invf_plt// ?posrE ?oppr_gt0// => NxV_lt_r.
+  apply: rA; last by rewrite invr_lt0.
+  by rewrite /= distrC subr0 ltr0_norm ?invr_lt0// -invrN.
+Qed.
+
 Section infty_nbhs_instances.
 Context {R : numFieldType}.
 Implicit Types r : R.
@@ -441,6 +488,20 @@ Unshelve. all: end_near. Qed.
 Lemma cvgNrNy f : (- f @ F --> -oo) <-> (f @ F --> +oo).
 Proof. by rewrite -cvgNry opprK. Qed.
 
+Lemma cvgryV f : f @ F --> +oo -> (f x)^-1 @[x --> F] --> (0 : R).
+Proof.
+move=> cvgy.
+apply: cvg_comp; first exact: cvgy.
+by rewrite pinftyV; exact: cvg_within.
+Qed.
+
+Lemma cvgrNyV f : f @ F --> -oo -> (f x)^-1 @[x --> F] --> (0 : R).
+Proof.
+move=> cvgNy.
+apply: cvg_comp; first exact: cvgNy.
+by rewrite ninftyV; exact: cvg_within.
+Qed.
+
 End cvg_infty_numField.
 
 Section cvg_infty_realField.
@@ -526,6 +587,31 @@ Proof. by move=> fy; under eq_fun do rewrite mulrC; exact: gt0_cvgMly. Qed.
 
 End gt0_cvg.
 
+Section lt0_cvg.
+Context {R : realFieldType} {F : set_system R} {FF : Filter F}.
+Variables (M : R) (f : R -> R).
+Hypothesis M0 : M < 0.
+
+Lemma lt0_cvgMlNy : (f r) @[r --> F] --> +oo -> (f r * M)%R @[r --> F] --> -oo.
+Proof.
+move=> /cvgryPge fy; apply/cvgrNyPle => A.
+by apply: filterS (fy (A / M)) => x; rewrite ler_ndivrMr.
+Qed.
+
+Lemma lt0_cvgMrNy : (f r) @[r --> F] --> +oo -> (M * f r)%R @[r --> F] --> -oo.
+Proof. by move=> fy; under eq_fun do rewrite mulrC; exact: lt0_cvgMlNy. Qed.
+
+Lemma lt0_cvgMly : f r @[r --> F] --> -oo -> (f r * M)%R @[r --> F] --> +oo.
+Proof.
+move=> /cvgrNyPle fNy; apply/cvgryPge => A.
+by apply: filterS (fNy (A / M)) => x; rewrite ler_ndivlMr.
+Qed.
+
+Lemma lt0_cvgMry : f r @[r --> F] --> -oo -> (M * f r)%R @[r --> F] --> +oo.
+Proof. by move=> fy; under eq_fun do rewrite mulrC; exact: lt0_cvgMly. Qed.
+
+End lt0_cvg.
+
 Lemma cvgNy_compNP {T : topologicalType} {R : numFieldType} (f : R -> T)
     (l : set_system T) :
   f x @[x --> -oo] --> l <-> (f \o -%R) x @[x --> +oo] --> l.
diff --git a/theories/normedtype_theory/pseudometric_normed_Zmodule.v b/theories/normedtype_theory/pseudometric_normed_Zmodule.v
index b1f779a5dc..3dfae5e38a 100644
--- a/theories/normedtype_theory/pseudometric_normed_Zmodule.v
+++ b/theories/normedtype_theory/pseudometric_normed_Zmodule.v
@@ -691,6 +691,22 @@ Proof.
 by rewrite at_leftN -?fmap_comp; under [_ \o _]eq_fun => ? do rewrite /= opprK.
 Qed.
 
+Lemma fmap_at_left0P {T : Type} {R : numFieldType} x (f : R -> T) : (f (x - e) @[e --> 0^'+]) = (f @ x^'-).
+Proof.
+rewrite -(subrr (-x)) at_right_shift at_rightN -fmap_comp.
+apply: near_eq_cvg_eq.
+apply: (nearW (F := x^'-)) => y /=.
+by rewrite opprB addNKr opprK.
+Qed.
+
+Lemma fmap_at_right0E {T : Type} {R : numFieldType} (x : R) (f : R -> T) : (f (x + e) @[e --> 0^'+]) = (f @ x^'+).
+Proof.
+rewrite -(subrr x) at_right_shift.
+apply: near_eq_cvg_eq.
+apply: (nearW (F := x^'+)) => y.
+by rewrite addrC subrK.
+Qed.
+
 Section at_left_right_pseudoMetricNormedZmod.
 Variables (R : numFieldType) (V : pseudoMetricNormedZmodType R).
 
diff --git a/theories/normedtype_theory/tvs.v b/theories/normedtype_theory/tvs.v
index 79719f209c..0f204fceaf 100644
--- a/theories/normedtype_theory/tvs.v
+++ b/theories/normedtype_theory/tvs.v
@@ -624,7 +624,6 @@ HB.instance Definition _ := Nbhs_isUniform_mixin.Build E
     entourage_inv entourage_split_ex
     nbhsE.
 
-
 HB.instance Definition _ := PreTopologicalNmodule_isTopologicalNmodule.Build E add_continuous.
 
 HB.instance Definition _ := TopologicalNmodule_isTopologicalLmodule.Build R E scale_continuous.
@@ -642,10 +641,26 @@ Proof. exact/nbhs0N_subproof/scale_continuous. Qed.
 Lemma nbhsT (x :E) : nbhs 0 U -> nbhs x (+%R x @` U).
 Proof. exact/nbhsT_subproof/add_continuous. Qed.
 
-Lemma nbhsB (z x : E) : nbhs z U -> nbhs (x + z) (+%R x @` U).
+End ConvexTvs_numDomain.
+
+Lemma nbhsB {R : numDomainType} {E : topologicalLmodType R} (U : set E)
+    (z x : E) :
+  nbhs z U -> nbhs (x + z) (+%R x @` U).
 Proof. exact/nbhsB_subproof/add_continuous. Qed.
 
-End ConvexTvs_numDomain.
+(* NB: similar to nbhsDl *)
+Lemma near_shiftE (R : numDomainType) (E : topologicalLmodType R) (U : set E) (x a : E) :
+  (\forall y \near x + a, U y) = (\near x, U (x + a)).
+Proof.
+eqProp; rewrite -!nbhs_nearE.
+- move/(nbhsB (-a)).
+  rewrite addrC addrK.
+  apply: filterS => _ [y Uy <-].
+  by rewrite addrC addNKr.
+- move/(nbhsB a); rewrite addrC.
+  apply: filterS => ? [y Uya <-].
+  by rewrite addrC.
+Qed.
 
 Section ConvexTvs_numField.
 
@@ -658,7 +673,7 @@ near=> x => //=; exists (r^-1 *: x); last by rewrite scalerA divff// scale1r.
 by apply: (BU (r^-1, x)); split => //=;[exact: nbhs_singleton|near: x].
 Unshelve. all: by end_near. Qed.
 
-Lemma nbhsZ  (R : numFieldType) (E : convexTvsType R) (U : set E) (r : R) (x :E) :
+Lemma nbhsZ (R : numFieldType) (E : convexTvsType R) (U : set E) (r : R) (x :E) :
   r != 0 -> nbhs x U -> nbhs (r *:x) ( *:%R r @` U ).
 Proof.
 move=> r0 U0; have /= := scale_continuous ((r^-1, r *: x)) U.
@@ -667,6 +682,20 @@ near=> z; exists (r^-1 *: z); last by rewrite scalerA divff// scale1r.
 by apply: (BU (r^-1,z)); split; [exact: nbhs_singleton|near: z].
 Unshelve. all: by end_near. Qed.
 
+Lemma nearZE (R : numFieldType) (T : convexTvsType R) (c : R) (x : T) (P : set T) :
+  c != 0 -> (\forall y \near c *: x, P y) = (\near x, P (c *: x)).
+Proof.
+move=> c_neq0.
+have cinv_neq0 : c^-1 != 0 by apply: invr_neq0.
+eqProp.
+- move/(nbhsZ cinv_neq0).
+  rewrite scalerK//.
+  apply: filterS => ? [y Py <-].
+  by rewrite scalerKV.
+- move/(nbhsZ c_neq0).
+  by apply: filterS => ? [y Pcy <-].
+Qed.
+
 End ConvexTvs_numField.
 
 Section standard_topology.
diff --git a/theories/topology_theory/num_topology.v b/theories/topology_theory/num_topology.v
index 5ef125b3a8..96f3fa58a7 100644
--- a/theories/topology_theory/num_topology.v
+++ b/theories/topology_theory/num_topology.v
@@ -464,6 +464,37 @@ move=> r/=; rewrite ltr_pdivlMr// -ltrBlDr; apply: le_lt_trans.
 by rewrite -lerBlDr opprK addrC (le_trans (ler_norm _))// ler_peMr// ler1n.
 Qed.
 
+Lemma near_right_in_itv {R : realFieldType} (a : R) (P : set R) :
+  (\forall b \near a^'+, {in `]a, b[, forall x, P x})
+  <-> {near a^'+, forall x, P x}.
+Proof.
+split=> [[/= _/posnumP[r] arP]|[/= r r0 arP]].
+- exists (r%:num / 2) => [//=|x /= /ltr_distlCDr xar2 ax].
+  apply: (arP (a + r%:num / 2)) => /=.
+  + by rewrite opprD addNKr normrN gtr0_norm// gtr_pMr// invf_lt1// ltr1n.
+  + by rewrite ltrDl.
+  + by rewrite in_itv/= ax.
+- exists r => // x /= /ltr_distlCDr xar ax y /[!in_itv]/= /andP[ay yx].
+  apply: arP => //=.
+  by rewrite distrC gtr0_norm ?subr_gt0// ltrBlDl (lt_trans _ xar).
+Qed.
+
+Lemma near_left_in_itv {R : realFieldType} (b : R) (P : set R) :
+  (\forall a \near b^'-, {in `]a, b[, forall x, P x})
+  <-> {near b^'-, forall x, P x}.
+Proof.
+split=> [[/= _/posnumP[r] brP]|[/= r r0 brP]].
+- exists (r%:num / 2) => [//=|x /= /ltr_distlDr bxr xb].
+  apply: (brP (b - r%:num / 2)) => /=.
+  + rewrite subKr gtr0_norm ?divr_gt0//.
+    by rewrite gtr_pMr// invf_plt ?posrE// invr1 ltrDl.
+  + by rewrite gtrBl divr_gt0.
+  + by rewrite in_itv/= xb andbT ltrBlDr.
+- exists r => // x /= /ltr_distlDr bxr xb y /[!in_itv]/= /andP[xy yb].
+  apply: brP => //=.
+  by rewrite gtr0_norm ?subr_gt0// ltrBlDl (lt_trans bxr)// ltrD2r.
+Qed.
+
 Section nbhs_lt_le.
 Context {R : numFieldType}.
 Implicit Types x z : R.