diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 9fee1fd696..1809a6f273 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -97,6 +97,9 @@
   + module `gauss_integral_proof`
   + lemma `integral0y_gauss`
 
+- in `normedtype.v`:
+  + lemmas `ninfty`, `cvgy_compNP`
+
 ### Changed
 
 - in `lebesgue_integral.v`
@@ -120,6 +123,9 @@
 - in file `separation_axioms.v`, updated `discrete_hausdorff`, and
     `discrete_zero_dimension` to take a `discreteTopologicalType`.
 
+- in `normedtype.v`:
+  + lemma `cvgyNP` renamed to `cvgNy_compN` and generalized
+
 ### Renamed
 
 - in `measure.v`
diff --git a/theories/normedtype.v b/theories/normedtype.v
index 686872e076..2968505c38 100644
--- a/theories/normedtype.v
+++ b/theories/normedtype.v
@@ -387,6 +387,14 @@ apply/seteqP; split => [A [M [Mreal MA]]|A [M [Mreal MA]]].
 by exists (- M); rewrite ?realN; split=> // x; rewrite ltrNr => /MA.
 Qed.
 
+Lemma ninfty {R : numFieldType} : (- x : R)%R @[x --> +oo] = -oo.
+Proof.
+apply/seteqP; split => [A [M [Mreal MA]]|A [M [Mreal MA]]].
+  exists (- M); rewrite realN; split => // x.
+  by rewrite -ltrNr => /MA/=; rewrite opprK.
+by exists (- M); rewrite ?realN; split=> // x; rewrite ltrNl => /MA.
+Qed.
+
 Section infty_nbhs_instances.
 Context {R : numFieldType}.
 Implicit Types r : R.
@@ -1476,13 +1484,23 @@ Proof.
 by rewrite at_leftN -?fmap_comp; under [_ \o _]eq_fun => ? do rewrite /= opprK.
 Qed.
 
-Lemma cvgyNP {T : topologicalType} {R : numFieldType}
-    (f : R -> T) (l : T) :
+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.
 Proof.
 have f_opp : f =1 (fun x => (f \o -%R) (- x)) by move=> x; rewrite /comp opprK.
 by rewrite (eq_cvg -oo _ f_opp) fmap_comp ninftyN.
 Qed.
+#[deprecated(since="mathcomp-analysis 1.9.0", note="renamed to `cvgNy_compNP`")]
+Notation cvgyNP := cvgNy_compNP (only parsing).
+
+Lemma cvgy_compNP {T : topologicalType} {R : numFieldType} (f : R -> T)
+    (l : set_system T) :
+  f x @[x --> +oo] --> l <-> (f \o -%R) x @[x --> -oo] --> l.
+Proof.
+have f_opp : f =1 (fun x => (f \o -%R) (- x)) by move=> x; rewrite /comp opprK.
+by rewrite (eq_cvg +oo _ f_opp) fmap_comp ninfty.
+Qed.
 
 Section open_itv_subset.
 Context {R : realType}.
diff --git a/theories/realfun.v b/theories/realfun.v
index 865431d671..173402202e 100644
--- a/theories/realfun.v
+++ b/theories/realfun.v
@@ -333,7 +333,7 @@ Lemma cvg_ninftyP (f : R -> R) (l : R) :
   f x @[x --> -oo] --> l <->
     forall u : R^nat, (u n @[n --> \oo] --> -oo) -> f (u n) @[n --> \oo] --> l.
 Proof.
-rewrite cvgyNP cvg_pinftyP/= (@bij_forall R^nat _ -%R)//.
+rewrite cvgNy_compNP cvg_pinftyP/= (@bij_forall R^nat _ -%R)//.
 have u_opp (u : R^nat) :
     ((- u) n @[n --> \oo] --> +oo) = (u n @[n --> \oo] --> -oo).
   by rewrite propeqE cvgNry.