From 31e13ee40df919e2cb4965477f7498a7b561a270 Mon Sep 17 00:00:00 2001
From: affeldt-aist <33154536+affeldt-aist@users.noreply.github.com>
Date: Fri, 10 Nov 2023 15:22:34 +0900
Subject: [PATCH] fixes #1052 (#1085)

---
 CHANGELOG_UNRELEASED.md      |  16 ++
 theories/charge.v            |   4 +-
 theories/esum.v              |   2 +-
 theories/kernel.v            |   2 +-
 theories/lebesgue_integral.v |  46 +++---
 theories/measure.v           |   2 +-
 theories/sequences.v         | 284 ++++++++++++++++++++---------------
 7 files changed, 207 insertions(+), 149 deletions(-)

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 092b3bf78..528c8b39a 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -160,6 +160,22 @@
   + `measurable_fun_lim_sup` -> `measurable_fun_limn_sup`
   + `measurable_fun_lim_esup` -> `measurable_fun_limn_esup`
 
+- in `sequences.v`:
+  + `ereal_nondecreasing_cvg` -> `ereal_nondecreasing_cvgn`
+  + `ereal_nondecreasing_is_cvg` -> `ereal_nondecreasing_is_cvgn`
+  + `ereal_nonincreasing_cvg` -> `ereal_nonincreasing_cvgn`
+  + `ereal_nonincreasing_is_cvg` -> `ereal_nonincreasing_is_cvgn`
+  + `ereal_nondecreasing_opp` -> `ereal_nondecreasing_oppn`
+  + `nonincreasing_cvg_ge` -> `nonincreasing_cvgn_ge`
+  + `nondecreasing_cvg_le` -> `nondecreasing_cvgn_le`
+  + `nonincreasing_cvg` -> `nonincreasing_cvgn`
+  + `nondecreasing_cvg` -> `nondecreasing_cvgn`
+  + `nonincreasing_is_cvg` -> `nonincreasing_is_cvgn`
+  + `nondecreasing_is_cvg` -> `nondecreasing_is_cvgn`
+  + `near_nonincreasing_is_cvg` -> `near_nonincreasing_is_cvgn`
+  + `near_nondecreasing_is_cvg` -> `near_nondecreasing_is_cvgn`
+  + `nondecreasing_dvg_lt` -> `nondecreasing_dvgn_lt`
+
 ### Generalized
 
 - in `topology.v`:
diff --git a/theories/charge.v b/theories/charge.v
index 11f336c25..e39b651cb 100644
--- a/theories/charge.v
+++ b/theories/charge.v
@@ -1027,12 +1027,12 @@ Lemma max_approxRN_seq_nd x : nondecreasing_seq (F_ ^~ x).
 Proof. by move=> a b ab; rewrite (le_bigmax_ord xpredT (g_ ^~ x)). Qed.
 
 Lemma is_cvg_max_approxRN_seq n : cvg (F_ ^~ n @ \oo).
-Proof. by apply: ereal_nondecreasing_is_cvg; exact: max_approxRN_seq_nd. Qed.
+Proof. by apply: ereal_nondecreasing_is_cvgn; exact: max_approxRN_seq_nd. Qed.
 
 Lemma is_cvg_int_max_approxRN_seq A :
   measurable A -> cvg ((fun n => \int[mu]_(x in A) F_ n x) @ \oo).
 Proof.
-move=> mA; apply: ereal_nondecreasing_is_cvg => a b ab.
+move=> mA; apply: ereal_nondecreasing_is_cvgn => a b ab.
 apply: ge0_le_integral => //.
 - by move=> ? ?; exact: max_approxRN_seq_ge0.
 - by apply: measurable_funS (measurable_max_approxRN_seq a).
diff --git a/theories/esum.v b/theories/esum.v
index 06625b351..95391f1e2 100644
--- a/theories/esum.v
+++ b/theories/esum.v
@@ -519,7 +519,7 @@ Lemma summable_cvg (P : pred nat) (f : (\bar R)^nat) :
   (forall i, P i -> 0 <= f i)%E -> summable P f ->
   cvg ((fun n => \sum_(0 <= k < n | P k) fine (f k))%R @ \oo).
 Proof.
-move=> f0 Pf; apply: nondecreasing_is_cvg.
+move=> f0 Pf; apply: nondecreasing_is_cvgn.
   by apply: nondecreasing_series => n Pn; exact/fine_ge0/f0.
 exists (fine (\sum_(i <oo | P i) `|f i|)) => x /= [n _ <-].
 rewrite summable_fine_sum// -lee_fin fineK//; last first.
diff --git a/theories/kernel.v b/theories/kernel.v
index 4a83cddb4..5ae016504 100644
--- a/theories/kernel.v
+++ b/theories/kernel.v
@@ -520,7 +520,7 @@ rewrite (_ : (fun x => _) =
   apply/funext => x.
   transitivity (lim (\int[l x]_y (k_ n (x, y))%:E @[n --> \oo])); last first.
     rewrite is_cvg_limn_esupE//.
-    apply: ereal_nondecreasing_is_cvg => m n mn.
+    apply: ereal_nondecreasing_is_cvgn => m n mn.
     apply: ge0_le_integral => //.
     - by move=> y _; rewrite lee_fin.
     - exact/EFin_measurable_fun/measurableT_comp.
diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v
index e483fc79a..ab23e880b 100644
--- a/theories/lebesgue_integral.v
+++ b/theories/lebesgue_integral.v
@@ -835,7 +835,7 @@ Lemma is_cvg_sintegral d (T : measurableType d) (R : realType)
   (m : {measure set T -> \bar R}) (f : {nnsfun T >-> R}^nat) :
   (forall x, nondecreasing_seq (f ^~ x)) -> cvgn (sintegral m \o f).
 Proof.
-move=> nd_f; apply/cvg_ex; eexists; apply/ereal_nondecreasing_cvg => a b ab.
+move=> nd_f; apply/cvg_ex; eexists; apply/ereal_nondecreasing_cvgn => a b ab.
 by apply: le_sintegral => // => x; exact/nd_f.
 Qed.
 
@@ -905,7 +905,7 @@ have [cf|df] := pselect (cvgn (g^~ x)).
   suff [n cfgn] : exists n, g n x >= c * f x by exists n.
   move/(@lt_lim _ _ _ (nd_g x) cf) : cfg => [n _ nf].
   by exists n; apply: nf => /=.
-have /cvgryPge/(_ (c * f x))[n _ ncfgn]:= nondecreasing_dvg_lt (nd_g x) df.
+have /cvgryPge/(_ (c * f x))[n _ ncfgn]:= nondecreasing_dvgn_lt (nd_g x) df.
 by exists n => //; rewrite /fleg /=; apply: ncfgn => /=.
 Qed.
 
@@ -985,9 +985,9 @@ apply/eqP; rewrite eq_le; apply/andP; split.
   by apply: nd_sintegral_lim_lemma => // x; rewrite -limg.
 have : nondecreasing_seq (sintegral mu \o g).
   by move=> m n mn; apply: le_sintegral => // x; exact/nd_g.
-move=> /ereal_nondecreasing_cvg/cvg_lim -> //.
+move=> /ereal_nondecreasing_cvgn/cvg_lim -> //.
 apply: ub_ereal_sup => _ [n _ <-] /=; apply: le_sintegral => // x.
-rewrite -limg // (nondecreasing_cvg_le (nd_g x)) //.
+rewrite -limg // (nondecreasing_cvgn_le (nd_g x)) //.
 by apply/cvg_ex; exists (f x); exact: gf.
 Qed.
 
@@ -1189,7 +1189,7 @@ apply/eqP; rewrite eq_le; apply/andP; split; last first.
   near=> n; apply: ereal_sup_ub; exists (g n) => //= => x.
   have <- : limn (EFin \o g ^~ x) = f x by apply/cvg_lim => //; exact: gf.
   have : EFin \o g ^~ x @ \oo --> ereal_sup (range (EFin \o g ^~ x)).
-    by apply: ereal_nondecreasing_cvg => p q pq /=; rewrite lee_fin; exact/nd_g.
+    by apply: ereal_nondecreasing_cvgn => p q pq /=; rewrite lee_fin; exact/nd_g.
   by move/cvg_lim => -> //; apply: ereal_sup_ub; exists n.
 have := leey (\int[mu]_x (f x)).
 rewrite le_eqVlt => /predU1P[|] mufoo; last first.
@@ -1524,7 +1524,7 @@ have nd_ag : {homo approx ^~ x : n m / (n <= m)%N >-> n <= m}.
 have fi0 y : D y -> (0 <= f y)%E by move=> ?; exact: f0.
 have cvg_af := cvg_approx fi0 Dx fixoo.
 have is_cvg_af : cvgn (approx ^~ x) by apply/cvg_ex; eexists; exact: cvg_af.
-have {is_cvg_af} := nondecreasing_cvg_le nd_ag is_cvg_af k.
+have {is_cvg_af} := nondecreasing_cvgn_le nd_ag is_cvg_af k.
 rewrite -lee_fin => /le_trans; apply.
 rewrite -(@fineK _ (f x)); last by rewrite ge0_fin_numE// f0.
 by move/(cvg_lim (@Rhausdorff R)) : cvg_af => ->.
@@ -1561,7 +1561,7 @@ move=> Dx; have := leey (f x); rewrite le_eqVlt => /predU1P[|] fxoo.
 have dvg_approx := dvg_approx Dx fxoo.
   have : {homo approx ^~ x : n m / (n <= m)%N >-> n <= m}.
     by move=> m n mn; have := nd_approx mn => /lefP; exact.
-  move/nondecreasing_dvg_lt => /(_ dvg_approx).
+  move/nondecreasing_dvgn_lt => /(_ dvg_approx).
   by rewrite fxoo => ?; apply/cvgeryP.
 rewrite -(@fineK _ (f x)); first exact: (cvg_comp (cvg_approx f0 Dx fxoo)).
 by rewrite ge0_fin_numE// f0.
@@ -1714,7 +1714,7 @@ have := gh1 t.
 rewrite -(fineK h1tfin) => /fine_cvgP[ft_near].
 set u_ := (X in X --> _) => u_h1 g1h1.
 have <- : lim u_ = fine (h1 t) by exact/cvg_lim.
-rewrite lee_fin; apply: nondecreasing_cvg_le.
+rewrite lee_fin; apply: nondecreasing_cvgn_le.
   by move=> // a b ab; rewrite /u_ /=; exact/lefP/nd_g1.
 by apply/cvg_ex; eexists; exact: u_h1.
 Unshelve. all: by end_near. Qed.
@@ -2110,7 +2110,9 @@ Qed.
 Let f := fun x => limn (g^~ x).
 
 Let is_cvg_g t : cvgn (g^~ t).
-Proof. by move=> ?; apply: ereal_nondecreasing_is_cvg => m n ?; apply/nd_g. Qed.
+Proof.
+by move=> ?; apply: ereal_nondecreasing_is_cvgn => m n ?; exact/nd_g.
+Qed.
 
 Local Definition g2' n : (T -> R)^nat := approx setT (g n).
 Local Definition g2 n : {nnsfun T >-> R}^nat := nnsfun_approx measurableT (mg n).
@@ -2122,7 +2124,7 @@ Local Definition max_g2 : {nnsfun T >-> R}^nat :=
 
 Let is_cvg_g2 n t : cvgn (EFin \o (g2 n ^~ t)).
 Proof.
-apply: ereal_nondecreasing_is_cvg => a b ab.
+apply: ereal_nondecreasing_is_cvgn => a b ab.
 by rewrite lee_fin 2!nnsfun_approxE; exact/lefP/nd_approx.
 Qed.
 
@@ -2141,7 +2143,7 @@ Qed.
 
 Let is_cvg_max_g2 t : cvgn (EFin \o max_g2 ^~ t).
 Proof.
-apply: ereal_nondecreasing_is_cvg => m n mn; rewrite lee_fin.
+apply: ereal_nondecreasing_is_cvgn => m n mn; rewrite lee_fin.
 exact/lefP/nd_max_g2.
 Qed.
 
@@ -2183,7 +2185,7 @@ have := leey (g n t); rewrite le_eqVlt => /predU1P[|] fntoo.
     under [in X in X --> _]eq_fun do rewrite nnsfun_approxE.
     have : {homo (approx setT (g n))^~ t : n0 m / (n0 <= m)%N >-> (n0 <= m)%R}.
       exact/lef_at/nd_approx.
-    by move/nondecreasing_dvg_lt => /(_ h).
+    by move/nondecreasing_dvgn_lt => /(_ h).
   have -> : limn (EFin \o max_g2 ^~ t) = +oo.
     by have := lim_g2_max_g2 t n; rewrite g2oo leye_eq => /eqP.
   by rewrite leey.
@@ -2214,18 +2216,18 @@ apply/eqP; rewrite eq_le; apply/andP; split; last first.
     - move=> x _; apply: lime_ge => //.
       by apply: nearW => k; exact/g0.
     - apply: emeasurable_fun_cvg mg _ => x _.
-      exact: ereal_nondecreasing_is_cvg.
+      exact: ereal_nondecreasing_is_cvgn.
     - move=> x Dx; apply: lime_ge => //.
       near=> m; have nm : (n <= m)%N by near: m; exists n.
       exact/nd_g.
-  by apply: lime_le => //; [exact:ereal_nondecreasing_is_cvg|exact:nearW].
+  by apply: lime_le => //; [exact:ereal_nondecreasing_is_cvgn|exact:nearW].
 rewrite (@nd_ge0_integral_lim _ _ _ mu _ max_g2) //; last 2 first.
   - move=> t; apply: lime_ge => //.
     by apply: nearW => n; exact: g0.
   - by move=> t m n mn; exact/lefP/nd_max_g2.
 apply: lee_lim.
 - by apply: is_cvg_sintegral => // t m n mn; exact/lefP/nd_max_g2.
-- apply: ereal_nondecreasing_is_cvg => // n m nm; apply: ge0_le_integral => //.
+- apply: ereal_nondecreasing_is_cvgn => // n m nm; apply: ge0_le_integral => //.
   by move=> *; exact/nd_g.
 - apply: nearW => n; rewrite ge0_integralTE//.
   by apply: ereal_sup_ub; exists (max_g2 n) => // t; exact: max_g2_g.
@@ -2234,7 +2236,7 @@ Unshelve. all: by end_near. Qed.
 Lemma cvg_monotone_convergence :
   \int[mu]_(x in D) g' n x @[n \oo] --> \int[mu]_(x in D) f' x.
 Proof.
-rewrite monotone_convergence; apply: ereal_nondecreasing_is_cvg => m n mn.
+rewrite monotone_convergence; apply: ereal_nondecreasing_is_cvgn => m n mn.
 by apply: ge0_le_integral => // t Dt; [exact: g'0|exact: g'0|exact: nd_g'].
 Qed.
 
@@ -2431,7 +2433,7 @@ rewrite (_ : \int[m]_(x in D) _ =
   - by move=> x _ a b /ndf_ /lefP; rewrite lee_fin.
 rewrite -limeMl//.
   by congr (limn _); apply/funext => n /=; rewrite integral_mscale_nnsfun.
-apply/ereal_nondecreasing_is_cvg => a b ab; apply: ge0_le_integral => //.
+apply/ereal_nondecreasing_is_cvgn => a b ab; apply: ge0_le_integral => //.
 - by move=> x _; rewrite lee_fin.
 - exact/EFin_measurable_fun/measurable_funTS.
 - by move=> x _; rewrite lee_fin.
@@ -2460,11 +2462,11 @@ rewrite monotone_convergence //; last first.
   move=> x Dx m n mn /=; apply: le_ereal_inf => _ /= [p /= np <-].
   by exists p => //=; rewrite (leq_trans mn).
 apply: lee_lim.
-- apply/cvg_ex; eexists; apply/ereal_nondecreasing_cvg => a b ab.
+- apply/cvg_ex; eexists; apply/ereal_nondecreasing_cvgn => a b ab.
   apply: ge0_le_integral => //; [exact: g0| exact: mg| exact: g0| exact: mg|].
   move=> x Dx; apply: le_ereal_inf => _ [n /= bn <-].
   by exists n => //=; rewrite (leq_trans ab).
-- apply/cvg_ex; eexists; apply/ereal_nondecreasing_cvg => a b ab.
+- apply/cvg_ex; eexists; apply/ereal_nondecreasing_cvgn => a b ab.
   apply: le_ereal_inf => // _ [n /= bn <-].
   by exists n => //=; rewrite (leq_trans ab).
 - apply: nearW => m.
@@ -2739,11 +2741,11 @@ have mf_ n : measurable_fun D (fun x => (f_ n x)%:E).
 have f_ge0 n x : D x -> 0 <= (f_ n x)%:E by move=> Dx; rewrite lee_fin.
 have cvg_f_ (m : {measure set T -> \bar R}) :
     cvgn (fun x => \int[m]_(x0 in D) (f_ x x0)%:E).
-  apply: ereal_nondecreasing_is_cvg => a b ab.
+  apply: ereal_nondecreasing_is_cvgn => a b ab.
   apply: ge0_le_integral => //; [exact: f_ge0|exact: f_ge0|].
   by move=> t Dt; rewrite lee_fin; apply/lefP/f_nd.
 transitivity (limn (fun n =>
-    \int[measure_add [the measure _ _ of msum m_ N] (m_ N)]_(x in D) (f_ n x)%:E)).
+    \int[measure_add (msum m_ N) (m_ N)]_(x in D) (f_ n x)%:E)).
   rewrite -monotone_convergence//; last first.
     by move=> t Dt a b ab; rewrite lee_fin; exact/lefP/f_nd.
   by apply: eq_integral => t /[!inE] Dt; apply/esym/cvg_lim => //; exact: f_f.
@@ -3215,7 +3217,7 @@ have lim_f_ t : f_ ^~ t @ \oo --> (f \_ D) t.
       by rewrite /f_ patchN// big_mkord big_ord0 inE/= in_set0.
     apply: ub_ereal_sup => x [n _ <-].
     by rewrite /f_ restrict_lee// big_mkord; exact: bigsetU_bigcup.
-  apply: ereal_nondecreasing_cvg => a b ab.
+  apply: ereal_nondecreasing_cvgn => a b ab.
   rewrite /f_ !big_mkord restrict_lee //; last exact: subset_bigsetU.
   by move=> x Dx; apply: f0 => //; exact: bigsetU_bigcup Dx.
 transitivity (\int[mu]_x limn (f_ ^~ x)).
diff --git a/theories/measure.v b/theories/measure.v
index e62d0fd4a..1a75e0d04 100644
--- a/theories/measure.v
+++ b/theories/measure.v
@@ -3566,7 +3566,7 @@ suff : forall n, \sum_(k < n) mu (X `&` A k) + mu (X `&` ~` A') <= mu X.
   move=> XA; rewrite (_ : limn _ = ereal_sup
       ((fun n => \sum_(k < n) mu (X `&` A k)) @` setT)); last first.
     under eq_fun do rewrite big_mkord.
-    apply/cvg_lim => //; apply: ereal_nondecreasing_cvg.
+    apply/cvg_lim => //; apply: ereal_nondecreasing_cvgn.
     apply: (lee_sum_nneg_ord (fun n => mu (X `&` A n)) xpredT) => n _.
     exact: outer_measure_ge0.
   move XAx : (mu (X `&` ~` A')) => [x| |].
diff --git a/theories/sequences.v b/theories/sequences.v
index 8ab2cf325..27870abb7 100644
--- a/theories/sequences.v
+++ b/theories/sequences.v
@@ -40,16 +40,16 @@ Require Import reals ereal signed topology normedtype landau.
 (*                                                                            *)
 (* Sections sequences_R_* contain properties of sequences of real numbers.    *)
 (* For example:                                                               *)
-(* nonincreasing_cvg_ge u_ == if u_ is nonincreasing and convergent then      *)
-(*                            forall n, lim u_ <= u_ n                        *)
-(* nondecreasing_cvg_le u_ == if u_ is nondecreasing and convergent then      *)
-(*                            forall n, lim u_ >= u_ n                        *)
-(*    nondecreasing_cvg u_ == if u_ is nondecreasing and bounded then u_      *)
-(*                            is convergent and its limit is sup u_n          *)
-(*    nonincreasing_cvg u_ == if u_ is nonincreasing u_ and bound by below    *)
-(*                            then u_ is convergent                           *)
-(*                adjacent == adjacent sequences lemma                        *)
-(*                  cesaro == Cesaro's lemma                                  *)
+(* nonincreasing_cvgn_ge u_ == if u_ is nonincreasing and convergent then     *)
+(*                             forall n, lim u_ <= u_ n                       *)
+(* nondecreasing_cvgn_le u_ == if u_ is nondecreasing and convergent then     *)
+(*                             forall n, lim u_ >= u_ n                       *)
+(*    nondecreasing_cvgn u_ == if u_ is nondecreasing and bounded then u_     *)
+(*                             is convergent and its limit is sup u_n         *)
+(*    nonincreasing_cvgn u_ == if u_ is nonincreasing u_ and bound by below   *)
+(*                             then u_ is convergent                          *)
+(*                 adjacent == adjacent sequences lemma                       *)
+(*                   cesaro == Cesaro's lemma                                 *)
 (*                                                                            *)
 (* * About sequences of natural numbers:                                      *)
 (*   nseries                                                                  *)
@@ -456,7 +456,7 @@ have : limn u <= M by apply: limr_le => //; near=> m; apply/ltW/Mu.
 by move/(lt_le_trans Ml); rewrite ltxx.
 Unshelve. all: by end_near. Qed.
 
-Lemma nonincreasing_cvg_ge u_ : nonincreasing_seq u_ -> cvgn u_ ->
+Lemma nonincreasing_cvgn_ge u_ : nonincreasing_seq u_ -> cvgn u_ ->
   forall n, limn u_ <= u_ n.
 Proof.
 move=> du ul p; rewrite leNgt; apply/negP => up0.
@@ -472,10 +472,10 @@ have : `|limn u_ - u_ N| >= `|u_ p - limn u_|%R.
 rewrite leNgt => /negP; apply; by near: N.
 Unshelve. all: by end_near. Qed.
 
-Lemma nondecreasing_cvg_le u_ : nondecreasing_seq u_ -> cvgn u_ ->
+Lemma nondecreasing_cvgn_le u_ : nondecreasing_seq u_ -> cvgn u_ ->
   forall n, u_ n <= limn u_.
 Proof.
-move=> iu cu n; move: (@nonincreasing_cvg_ge (- u_)).
+move=> iu cu n; move: (@nonincreasing_cvgn_ge (- u_)).
 rewrite -nondecreasing_opp opprK => /(_ iu); rewrite is_cvgNE => /(_ cu n).
 by rewrite limN // lerNl opprK.
 Qed.
@@ -538,6 +538,12 @@ Proof. exact: cvgrNyPltNy. Qed.
 Notation cvgPninfty_lt_near := __deprecated__cvgPninfty_lt_near (only parsing).
 
 End sequences_R_lemmas_realFieldType.
+#[deprecated(since="mathcomp-analysis 0.6.6",
+  note="renamed to `nonincreasing_cvgn_ge`")]
+Notation nonincreasing_cvg_ge := nonincreasing_cvgn_ge (only parsing).
+#[deprecated(since="mathcomp-analysis 0.6.6",
+  note="renamed to `nondecreasing_cvgn_le`")]
+Notation nondecreasing_cvg_le := nondecreasing_cvgn_le (only parsing).
 
 Lemma __deprecated__invr_cvg0 (R : realFieldType) (u : R^nat) :
   (forall i, 0 < u i) -> ((u i)^-1 @[i --> \oo] --> 0) <-> (u @ \oo --> +oo).
@@ -679,7 +685,7 @@ End series_patched.
 Section sequences_R_lemmas.
 Variable R : realType.
 
-Lemma nondecreasing_cvg (u_ : R ^nat) :
+Lemma nondecreasing_cvgn (u_ : R ^nat) :
     nondecreasing_seq u_ -> has_ubound (range u_) ->
   u_ @ \oo --> sup (range u_).
 Proof.
@@ -694,51 +700,50 @@ rewrite ler_distlC (le_trans Mu_p (leu _ _ _))//= (@le_trans _ _ M) ?lerDl//.
 by have /ubP := sup_upper_bound su_; apply; exists n.
 Unshelve. all: by end_near. Qed.
 
-Lemma nondecreasing_is_cvg (u_ : R ^nat) :
+Lemma nondecreasing_is_cvgn (u_ : R ^nat) :
   nondecreasing_seq u_ -> has_ubound (range u_) -> cvgn u_.
-Proof. by move=> u_nd u_ub; apply: cvgP; apply: nondecreasing_cvg. Qed.
+Proof. by move=> u_nd u_ub; apply: cvgP; exact: nondecreasing_cvgn. Qed.
 
-Lemma nondecreasing_dvg_lt (u_ : R ^nat) :
+Lemma nondecreasing_dvgn_lt (u_ : R ^nat) :
   nondecreasing_seq u_ -> ~ cvgn u_ -> u_ @ \oo --> +oo.
 Proof.
 move=> nu du; apply: contrapT => /cvgryPge/existsNP[l lu]; apply: du.
-apply: nondecreasing_is_cvg => //; exists l => _ [n _ <-].
+apply: nondecreasing_is_cvgn => //; exists l => _ [n _ <-].
 rewrite leNgt; apply/negP => lun; apply: lu; near=> m.
 by rewrite (le_trans (ltW lun)) //; apply: nu; near: m; exists n.
 Unshelve. all: by end_near. Qed.
 
-Lemma near_nondecreasing_is_cvg (u_ : R ^nat) (M : R) :
+Lemma near_nondecreasing_is_cvgn (u_ : R ^nat) (M : R) :
     {near \oo, nondecreasing_seq u_} -> (\forall n \near \oo, u_ n <= M) ->
   cvgn u_.
 Proof.
 move=> [k _ u_nd] [k' _ u_M].
 suff : cvgn [sequence u_ (n + maxn k k')%N]_n.
   by case/cvg_ex => /= l; rewrite cvg_shiftn => ul; apply/cvg_ex; exists l.
-apply: nondecreasing_is_cvg; [move=> /= m n mn|exists M => _ [n _ <-]].
+apply: nondecreasing_is_cvgn; [move=> /= m n mn|exists M => _ [n _ <-]].
   by rewrite u_nd ?leq_add2r//= (leq_trans (leq_maxl _ _) (leq_addl _ _)).
 by rewrite u_M //= (leq_trans (leq_maxr _ _) (leq_addl _ _)).
 Qed.
 
-Lemma nonincreasing_cvg (u_ : R ^nat) :
+Lemma nonincreasing_cvgn (u_ : R ^nat) :
     nonincreasing_seq u_ -> has_lbound (range u_) ->
   u_ @ \oo --> inf (u_ @` setT).
 Proof.
-rewrite -nondecreasing_opp => u_nd u_lb.
-rewrite -[X in X @ \oo --> _](opprK u_).
-apply: cvgN; rewrite image_comp; apply: nondecreasing_cvg => //.
+rewrite -nondecreasing_opp => u_nd u_lb; rewrite -[X in X @ _ --> _](opprK u_).
+apply: cvgN; rewrite image_comp; apply: nondecreasing_cvgn => //.
 by move/has_lb_ubN : u_lb; rewrite image_comp.
 Qed.
 
-Lemma nonincreasing_is_cvg (u_ : R ^nat) :
+Lemma nonincreasing_is_cvgn (u_ : R ^nat) :
   nonincreasing_seq u_ -> has_lbound (range u_) -> cvgn u_.
-Proof. by move=> u_decr u_bnd; apply: cvgP; apply: nonincreasing_cvg. Qed.
+Proof. by move=> u_decr u_bnd; apply: cvgP; exact: nonincreasing_cvgn. Qed.
 
-Lemma near_nonincreasing_is_cvg (u_ : R ^nat) (m : R) :
+Lemma near_nonincreasing_is_cvgn (u_ : R ^nat) (m : R) :
     {near \oo, nonincreasing_seq u_} -> (\forall n \near \oo, m <= u_ n) ->
   cvgn u_.
 Proof.
 move=> u_ni u_m.
-rewrite -(opprK u_); apply: is_cvgN; apply/(@near_nondecreasing_is_cvg _ (- m)).
+rewrite -(opprK u_); apply: is_cvgN; apply/(@near_nondecreasing_is_cvgn _ (- m)).
 - by apply: filterS u_ni => x u_x y xy; rewrite lerNl opprK u_x.
 - by apply: filterS u_m => x u_x; rewrite lerNl opprK.
 Qed.
@@ -749,18 +754,39 @@ Lemma adjacent (u_ v_ : R ^nat) : nondecreasing_seq u_ -> nonincreasing_seq v_ -
 Proof.
 set w_ := v_ - u_ => iu dv w0; have vu n : v_ n >= u_ n.
   suff : limn w_ <= w_ n by rewrite (cvg_lim _ w0)// subr_ge0.
-  apply: (nonincreasing_cvg_ge _ (cvgP _ w0)) => m p mp.
+  apply: (nonincreasing_cvgn_ge _ (cvgP _ w0)) => m p mp.
   by rewrite lerB; rewrite ?iu ?dv.
 have cu : cvgn u_.
-  apply: nondecreasing_is_cvg => //; exists (v_ 0%N) => _ [n _ <-].
+  apply: nondecreasing_is_cvgn => //; exists (v_ 0%N) => _ [n _ <-].
   by rewrite (le_trans (vu _)) // dv.
 have cv : cvgn v_.
-  apply: nonincreasing_is_cvg => //; exists (u_ 0%N) => _ [n _ <-].
+  apply: nonincreasing_is_cvgn => //; exists (u_ 0%N) => _ [n _ <-].
   by rewrite (le_trans _ (vu _)) // iu.
 by split=> //; apply/eqP; rewrite -subr_eq0 -limB //; exact/eqP/cvg_lim.
 Qed.
 
 End sequences_R_lemmas.
+#[deprecated(since="mathcomp-analysis 0.6.6",
+  note="renamed to `nonincreasing_cvgn`")]
+Notation nonincreasing_cvg := nonincreasing_cvgn (only parsing).
+#[deprecated(since="mathcomp-analysis 0.6.6",
+  note="renamed to `nondecreasing_cvgn`")]
+Notation nondecreasing_cvg := nondecreasing_cvgn (only parsing).
+#[deprecated(since="mathcomp-analysis 0.6.6",
+  note="renamed to `nonincreasing_is_cvgn`")]
+Notation nonincreasing_is_cvg := nonincreasing_is_cvgn (only parsing).
+#[deprecated(since="mathcomp-analysis 0.6.6",
+  note="renamed to `nondecreasing_is_cvgn`")]
+Notation nondecreasing_is_cvg := nondecreasing_is_cvgn (only parsing).
+#[deprecated(since="mathcomp-analysis 0.6.6",
+  note="renamed to `nondecreasing_dvgn_lt`")]
+Notation nondecreasing_dvg_lt := nondecreasing_dvgn_lt (only parsing).
+#[deprecated(since="mathcomp-analysis 0.6.6",
+  note="renamed to `near_nondecreasing_is_cvgn`")]
+Notation near_nondecreasing_is_cvg := near_nondecreasing_is_cvgn (only parsing).
+#[deprecated(since="mathcomp-analysis 0.6.6",
+  note="renamed to `near_nonincreasing_is_cvgn`")]
+Notation near_nonincreasing_is_cvg := near_nonincreasing_is_cvgn (only parsing).
 
 Definition harmonic {R : fieldType} : R ^nat := [sequence n.+1%:R^-1]_n.
 Arguments harmonic {R} n /.
@@ -1077,7 +1103,7 @@ Lemma series_le_cvg (R : realType) (u_ v_ : R ^nat) :
   cvgn (series v_) -> cvgn (series u_).
 Proof.
 move=> u_ge0 v_ge0 le_uv /cvg_seq_bounded/bounded_fun_has_ubound[M v_M].
-apply: nondecreasing_is_cvg; first exact: nondecreasing_series.
+apply: nondecreasing_is_cvgn; first exact: nondecreasing_series.
 exists M => _ [n _ <-].
 by apply: le_trans (v_M (series v_ n) _); [apply: ler_sum | exists n].
 Qed.
@@ -1228,7 +1254,7 @@ Lemma is_cvg_series_exp_coeff_pos : cvgn (series (exp x)).
 Proof.
 rewrite /series; near \oo => N; have xN : x < N%:R; last first.
   rewrite -(@is_cvg_series_restrict N.+1).
-  by apply: (nondecreasing_is_cvg (incr_S1 N)); eexists; apply: S1_sup.
+  by apply: (nondecreasing_is_cvgn (incr_S1 N)); eexists; apply: S1_sup.
 near: N; exists (absz (floor x)).+1 => // m; rewrite /mkset -(@ler_nat R).
 move/lt_le_trans => -> //; rewrite (lt_le_trans (lt_succ_floor x)) // -addn1.
 by rewrite natrD lerD2r -(@gez0_abs (floor x)) ?floor_ge0// ltW.
@@ -1418,7 +1444,7 @@ Local Open Scope ereal_scope.
 Variable T : realDomainType.
 Implicit Types u : (\bar T)^nat.
 
-Lemma ereal_nondecreasing_opp u_ :
+Lemma ereal_nondecreasing_oppn u_ :
   nondecreasing_seq (-%E \o u_) = nonincreasing_seq u_.
 Proof.
 rewrite propeqE; split => ni_u m n mn; last by rewrite lee_oppr oppeK ni_u.
@@ -1426,6 +1452,9 @@ by rewrite -(oppeK (u_ m)) -lee_oppr ni_u.
 Qed.
 
 End sequences_ereal_realDomainType.
+#[deprecated(since="mathcomp-analysis 0.6.6",
+  note="renamed to `ereal_nondecreasing_oppn`")]
+Notation ereal_nondecreasing_opp := ereal_nondecreasing_oppn (only parsing).
 
 Section sequences_ereal.
 Local Open Scope ereal_scope.
@@ -1433,46 +1462,29 @@ Local Open Scope ereal_scope.
 Lemma __deprecated__ereal_cvg_abs0 (R : realFieldType) (f : (\bar R)^nat) :
   abse \o f @ \oo --> 0 -> f @ \oo --> 0.
 Proof. by move/cvg_abse0P. Qed.
-#[deprecated(since="mathcomp-analysis 0.6.0",
-  note="renamed to `cvg_abse0P` and generalized")]
-Notation ereal_cvg_abs0 := __deprecated__ereal_cvg_abs0 (only parsing).
 
 Lemma __deprecated__ereal_cvg_ge0 (R : realFieldType) (f : (\bar R)^nat) (a : \bar R) :
   (forall n, 0 <= f n) -> f @ \oo --> a -> 0 <= a.
 Proof. by move=> f_ge0; apply: cvge_ge; apply: nearW. Qed.
-#[deprecated(since="mathcomp-analysis 0.6.0", note="use `cvge_ge` instead")]
-Notation ereal_cvg_ge0 := __deprecated__ereal_cvg_ge0 (only parsing).
 
 Lemma __deprecated__ereal_lim_ge (R : realFieldType) x (u_ : (\bar R)^nat) :
   cvgn u_ -> (\forall n \near \oo, x <= u_ n) -> x <= limn u_.
 Proof. exact: lime_ge. Qed.
-#[deprecated(since="mathcomp-analysis 0.6.0",
-  note="renamed to `lime_ge` and generalized")]
-Notation ereal_lim_ge := __deprecated__ereal_lim_ge (only parsing).
 
 Lemma __deprecated__ereal_lim_le (R : realFieldType) x (u_ : (\bar R)^nat) :
   cvgn u_ -> (\forall n \near \oo, u_ n <= x) -> limn u_ <= x.
 Proof. exact: lime_le. Qed.
-#[deprecated(since="mathcomp-analysis 0.6.0",
-  note="renamed to `lime_le` and generalized")]
-Notation ereal_lim_le := __deprecated__ereal_lim_le (only parsing).
 
 Lemma __deprecated__dvg_ereal_cvg (R : realFieldType) (u_ : R ^nat) :
   u_ @ \oo --> +oo%R -> [sequence (u_ n)%:E]_n @ \oo --> +oo.
 Proof. by rewrite cvgeryP. Qed.
-#[deprecated(since="mathcomp-analysis 0.6.0",
-  note="renamed to `cvgeryP` and generalized")]
-Notation dvg_ereal_cvg := __deprecated__dvg_ereal_cvg (only parsing).
 
 Lemma __deprecated__ereal_cvg_real (R : realFieldType) (f : (\bar R)^nat) a :
   {near \oo, forall x, f x \is a fin_num} /\
   (fine \o f @ \oo --> a) <-> f @ \oo --> a%:E.
 Proof. by rewrite fine_cvgP. Qed.
-#[deprecated(since="mathcomp-analysis 0.6.0",
-  note="renamed to `fine_cvgP` and generalized")]
-Notation ereal_cvg_real := __deprecated__ereal_cvg_real (only parsing).
 
-Lemma ereal_nondecreasing_cvg (R : realType) (u_ : (\bar R)^nat) :
+Lemma ereal_nondecreasing_cvgn (R : realType) (u_ : (\bar R)^nat) :
   nondecreasing_seq u_ -> u_ @ \oo --> ereal_sup (u_ @` setT).
 Proof.
 move=> nd_u_; set S := u_ @` setT; set l := ereal_sup S.
@@ -1520,7 +1532,7 @@ have <- : sup (range v_) = fine l.
   rewrite (@le_trans _ _ (u_ (m + N)%N))//; first by rewrite nd_u_// leq_addr.
   apply: ereal_sup_ub => /=; exists (fine (u_ (m + N)%N)); first by exists m.
   by rewrite fineK// u_fin_num// leq_addl.
-apply: nondecreasing_cvg.
+apply: nondecreasing_cvgn.
 - move=> m n mn /=; rewrite /v_ /= fine_le ?u_fin_num ?leq_addl//.
   by rewrite nd_u_// leq_add2r.
 - exists (fine l) => /= _ [m _ <-]; rewrite /v_ /= fine_le//.
@@ -1528,11 +1540,11 @@ apply: nondecreasing_cvg.
   by apply: ereal_sup_ub; exists (m + N)%N.
 Unshelve. all: by end_near. Qed.
 
-Lemma ereal_nondecreasing_is_cvg (R : realType) (u_ : (\bar R) ^nat) :
+Lemma ereal_nondecreasing_is_cvgn (R : realType) (u_ : (\bar R) ^nat) :
   nondecreasing_seq u_ -> cvgn u_.
-Proof. by move=> ?; apply/cvg_ex; eexists; exact: ereal_nondecreasing_cvg. Qed.
+Proof. by move=> ?; apply/cvg_ex; eexists; exact: ereal_nondecreasing_cvgn. Qed.
 
-Lemma ereal_nonincreasing_cvg (R : realType) (u_ : (\bar R)^nat) :
+Lemma ereal_nonincreasing_cvgn (R : realType) (u_ : (\bar R)^nat) :
   nonincreasing_seq u_ -> u_ @ \oo --> ereal_inf (u_ @` setT).
 Proof.
 move=> ni_u; rewrite [X in X @ \oo --> _](_ : _ = -%E \o -%E \o u_); last first.
@@ -1541,12 +1553,12 @@ apply: cvgeN.
 rewrite [X in _ --> X](_ : _ = ereal_sup (range (-%E \o u_))); last first.
   congr ereal_sup; rewrite predeqE => x; split=> [[_ [n _ <-]] <-|[n _] <-];
     by [exists n | exists (u_ n) => //; exists n].
-by apply: ereal_nondecreasing_cvg; rewrite ereal_nondecreasing_opp.
+by apply: ereal_nondecreasing_cvgn; rewrite ereal_nondecreasing_oppn.
 Qed.
 
-Lemma ereal_nonincreasing_is_cvg (R : realType) (u_ : (\bar R) ^nat) :
+Lemma ereal_nonincreasing_is_cvgn (R : realType) (u_ : (\bar R) ^nat) :
   nonincreasing_seq u_ -> cvgn u_.
-Proof. by move=> ?; apply/cvg_ex; eexists; apply: ereal_nonincreasing_cvg. Qed.
+Proof. by move=> ?; apply/cvg_ex; eexists; apply: ereal_nonincreasing_cvgn. Qed.
 
 (* NB: see also nondecreasing_series *)
 Lemma ereal_nondecreasing_series (R : realDomainType) (u_ : (\bar R)^nat)
@@ -1558,15 +1570,15 @@ Lemma congr_lim (R : numFieldType) (f g : nat -> \bar R) :
   f = g -> limn f = limn g.
 Proof. by move=> ->. Qed.
 
-Lemma eseries_cond {R : numFieldType} (f : nat -> \bar R) P N :
+Lemma eseries_cond {R : numFieldType} (f : (\bar R)^nat) P N :
   \sum_(N <= i <oo | P i) f i = \sum_(i <oo | P i && (N <= i)%N) f i.
 Proof. by apply/congr_lim/eq_fun => n /=; apply: big_nat_widenl. Qed.
 
-Lemma eseries_mkcondl {R : numFieldType} (f : nat -> \bar R) P Q :
+Lemma eseries_mkcondl {R : numFieldType} (f : (\bar R)^nat) P Q :
   \sum_(i <oo | P i && Q i) f i = \sum_(i <oo | Q i) if P i then f i else 0.
 Proof. by apply/congr_lim/funext => n; rewrite big_mkcondl. Qed.
 
-Lemma eseries_mkcondr {R : numFieldType} (f : nat -> \bar R) P Q :
+Lemma eseries_mkcondr {R : numFieldType} (f : (\bar R)^nat) P Q :
   \sum_(i <oo | P i && Q i) f i = \sum_(i <oo | P i) if Q i then f i else 0.
 Proof. by apply/congr_lim/funext => n; rewrite big_mkcondr. Qed.
 
@@ -1613,7 +1625,7 @@ Lemma nneseries_lim_ge (R : realType) (u_ : (\bar R)^nat) (P : pred nat) k :
   (forall n, P n -> 0 <= u_ n) ->
   \sum_(0 <= i < k | P i) u_ i <= \sum_(i <oo | P i) u_ i.
 Proof.
-move/ereal_nondecreasing_series/ereal_nondecreasing_cvg/cvg_lim => -> //.
+move/ereal_nondecreasing_series/ereal_nondecreasing_cvgn/cvg_lim => -> //.
 by apply: ereal_sup_ub; exists k.
 Qed.
 
@@ -1637,14 +1649,14 @@ Lemma is_cvg_ereal_nneg_natsum_cond m P :
     (forall n, (m <= n)%N -> P n -> 0 <= u_ n) ->
   cvgn (fun n => \sum_(m <= i < n | P i) u_ i).
 Proof.
-by move/lee_sum_nneg_natr/ereal_nondecreasing_cvg => cu; apply: cvgP; exact: cu.
+by move/lee_sum_nneg_natr/ereal_nondecreasing_cvgn => cu; apply: cvgP; exact: cu.
 Qed.
 
 Lemma is_cvg_ereal_npos_natsum_cond m P :
     (forall n, (m <= n)%N -> P n -> u_ n <= 0) ->
   cvgn (fun n => \sum_(m <= i < n | P i) u_ i).
 Proof.
-by move/lee_sum_npos_natr/ereal_nonincreasing_cvg => cu; apply: cvgP; exact: cu.
+by move/lee_sum_npos_natr/ereal_nonincreasing_cvgn => cu; apply: cvgP; exact: cu.
 Qed.
 
 Lemma is_cvg_ereal_nneg_natsum m : (forall n, (m <= n)%N -> 0 <= u_ n) ->
@@ -1695,7 +1707,7 @@ Lemma nnseries_is_cvg {R : realType} (u : nat -> R) :
     (forall i, 0 <= u i)%R -> \sum_(k <oo) (u k)%:E < +oo ->
   cvgn (series u).
 Proof.
-move=> ? ?; apply: nondecreasing_is_cvg.
+move=> ? ?; apply: nondecreasing_is_cvgn.
   move=> m n mn; rewrite /series/=.
   rewrite -(subnKC mn) {2}/index_iota subn0 iotaD big_cat/=.
   by rewrite add0n -{2}(subn0 m) -/(index_iota _ _) lerDl sumr_ge0.
@@ -1729,26 +1741,17 @@ Lemma __deprecated__ereal_cvgPpinfty (R : realFieldType) (u_ : (\bar R)^nat) :
 Proof.
 by split=> [/cvgeyPge//|u_ge]; apply/cvgeyPgey; near=> x; apply: u_ge.
 Unshelve. all: by end_near. Qed.
-#[deprecated(since="mathcomp-analysis 0.6.0",
-  note="use `cvgeyPge` or a variant instead")]
-Notation ereal_cvgPpinfty := __deprecated__ereal_cvgPpinfty (only parsing).
 
 Lemma __deprecated__ereal_cvgPninfty (R : realFieldType) (u_ : (\bar R)^nat) :
   u_ @ \oo --> -oo <-> (forall A, (A < 0)%R -> \forall n \near \oo, u_ n <= A%:E).
 Proof.
 by split=> [/cvgeNyPle//|u_ge]; apply/cvgeNyPleNy; near=> x; apply: u_ge.
 Unshelve. all: by end_near. Qed.
-#[deprecated(since="mathcomp-analysis 0.6.0",
-  note="use `cvgeNyPle` or a variant instead")]
-Notation ereal_cvgPninfty := __deprecated__ereal_cvgPninfty (only parsing).
 
 Lemma __deprecated__ereal_squeeze (R : realType) (f g h : (\bar R)^nat) :
   (\forall x \near \oo, f x <= g x <= h x) -> forall (l : \bar R),
   f @ \oo --> l -> h @ \oo --> l -> g @ \oo --> l.
 Proof. by move=> ? ?; apply: squeeze_cvge. Qed.
-#[deprecated(since="mathcomp-analysis 0.6.0",
-  note="renamed to `squeeze_cvge` and generalized")]
-Notation ereal_squeeze := __deprecated__ereal_squeeze (only parsing).
 
 Lemma nneseries_pinfty (R : realType) (u_ : (\bar R)^nat)
   (P : pred nat) k : (forall n, P n -> 0 <= u_ n) -> P k ->
@@ -1784,20 +1787,14 @@ Unshelve. all: by end_near. Qed.
 Lemma __deprecated__ereal_cvgD_pinfty_fin (R : realFieldType) (f g : (\bar R)^nat) b :
   f @ \oo --> +oo -> g @ \oo --> b%:E -> f \+ g @ \oo --> +oo.
 Proof. exact: cvgeD. Qed.
-#[deprecated(since="mathcomp-analysis 0.6.0", note="use `cvgeD` instead")]
-Notation ereal_cvgD_pinfty_fin := __deprecated__ereal_cvgD_pinfty_fin (only parsing).
 
 Lemma __deprecated__ereal_cvgD_ninfty_fin (R : realFieldType) (f g : (\bar R)^nat) b :
   f @ \oo --> -oo -> g @ \oo --> b%:E -> f \+ g @ \oo --> -oo.
 Proof. exact: cvgeD. Qed.
-#[deprecated(since="mathcomp-analysis 0.6.0", note="use `cvgeD` instead")]
-Notation ereal_cvgD_ninfty_fin := __deprecated__ereal_cvgD_ninfty_fin (only parsing).
 
 Lemma __deprecated__ereal_cvgD_pinfty_pinfty (R : realFieldType) (f g : (\bar R)^nat) :
   f @ \oo --> +oo -> g @ \oo --> +oo -> f \+ g @ \oo --> +oo.
 Proof. exact: cvgeD. Qed.
-#[deprecated(since="mathcomp-analysis 0.6.0", note="use `cvgeD` instead")]
-Notation ereal_cvgD_pinfty_pinfty := __deprecated__ereal_cvgD_pinfty_pinfty (only parsing).
 
 Lemma __deprecated__ereal_cvgD_ninfty_ninfty (R : realFieldType) (f g : (\bar R)^nat) :
   f @ \oo --> -oo -> g @ \oo --> -oo -> f \+ g @ \oo --> -oo.
@@ -1808,40 +1805,25 @@ Notation ereal_cvgD_ninfty_ninfty := __deprecated__ereal_cvgD_ninfty_ninfty (onl
 Lemma __deprecated__ereal_cvgD (R : realFieldType) (f g : (\bar R)^nat) a b :
   a +? b -> f @ \oo --> a -> g @ \oo --> b -> f \+ g @ \oo --> a + b.
 Proof. exact: cvgeD. Qed.
-#[deprecated(since="mathcomp-analysis 0.6.0",
-  note="renamed to `cvgeD` and generalized")]
-Notation ereal_cvgD := __deprecated__ereal_cvgD (only parsing).
 
 Section nneseries_split.
 
 Lemma __deprecated__ereal_cvgB (R : realFieldType) (f g : (\bar R)^nat) a b :
   a +? - b -> f @ \oo --> a -> g @ \oo --> b -> f \- g @ \oo --> a - b.
 Proof. exact: cvgeB. Qed.
-#[deprecated(since="mathcomp-analysis 0.6.0",
-  note="renamed to `cvgeB` and generalized")]
-Notation ereal_cvgB := __deprecated__ereal_cvgB (only parsing).
 
 Lemma __deprecated__ereal_is_cvgD (R : realFieldType) (u v : (\bar R)^nat) :
     limn u +? limn v -> cvgn u -> cvgn v -> cvgn (u \+ v).
 Proof. exact: is_cvgeD. Qed.
-#[deprecated(since="mathcomp-analysis 0.6.0",
-  note="renamed to `is_cvgeD` and generalized")]
-Notation ereal_is_cvgD := __deprecated__ereal_is_cvgD (only parsing).
 
 Lemma __deprecated__ereal_cvg_sub0 (R : realFieldType) (f : (\bar R)^nat) (k : \bar R) :
   k \is a fin_num -> (fun x => f x - k) @ \oo --> 0 <-> f @ \oo --> k.
 Proof. exact: cvge_sub0. Qed.
-#[deprecated(since="mathcomp-analysis 0.6.0",
-  note="renamed to `cvge_sub0` and generalized")]
-Notation ereal_cvg_sub0 := __deprecated__ereal_cvg_sub0 (only parsing).
 
 Lemma __deprecated__ereal_limD (R : realFieldType) (f g : (\bar R)^nat) :
   cvgn f -> cvgn g -> limn f +? limn g ->
   limn (f \+ g) = limn f + limn g.
 Proof. exact: limeD. Qed.
-#[deprecated(since="mathcomp-analysis 0.6.0",
-  note="renamed to `limeD` and generalized")]
-Notation ereal_limD := __deprecated__ereal_limD (only parsing).
 
 Lemma __deprecated__ereal_cvgM_gt0_pinfty (R : realFieldType) (f g : (\bar R)^nat) b :
   (0 < b)%R -> f @ \oo --> +oo -> g @ \oo --> b%:E -> f \* g @ \oo --> +oo.
@@ -1849,8 +1831,6 @@ Proof.
 move=> b_lt0 fl gl; have /= := cvgeM _ fl gl; rewrite gt0_mulye//; apply.
 by rewrite mule_def_infty_neq0// gt_eqF.
 Qed.
-#[deprecated(since="mathcomp-analysis 0.6.0", note="use `cvgeM` instead")]
-Notation ereal_cvgM_gt0_pinfty := __deprecated__ereal_cvgM_gt0_pinfty (only parsing).
 
 Lemma __deprecated__ereal_cvgM_lt0_pinfty (R : realFieldType) (f g : (\bar R)^nat) b :
   (b < 0)%R -> f @ \oo --> +oo -> g @ \oo --> b%:E -> f \* g @ \oo --> -oo.
@@ -1858,8 +1838,6 @@ Proof.
 move=> b_lt0 fl gl; have /= := cvgeM _ fl gl; rewrite lt0_mulye//; apply.
 by rewrite mule_def_infty_neq0// lt_eqF.
 Qed.
-#[deprecated(since="mathcomp-analysis 0.6.0", note="use `cvgeM` instead")]
-Notation ereal_cvgM_lt0_pinfty := __deprecated__ereal_cvgM_lt0_pinfty (only parsing).
 
 Lemma __deprecated__ereal_cvgM_gt0_ninfty (R : realFieldType) (f g : (\bar R)^nat) b :
   (0 < b)%R -> f @ \oo --> -oo -> g @ \oo --> b%:E -> f \* g @ \oo --> -oo.
@@ -1867,8 +1845,6 @@ Proof.
 move=> b_lt0 fl gl; have /= := cvgeM _ fl gl; rewrite gt0_mulNye//; apply.
 by rewrite mule_def_infty_neq0// gt_eqF.
 Qed.
-#[deprecated(since="mathcomp-analysis 0.6.0", note="use `cvgeM` instead")]
-Notation ereal_cvgM_gt0_ninfty := __deprecated__ereal_cvgM_gt0_ninfty (only parsing).
 
 Lemma __deprecated__ereal_cvgM_lt0_ninfty (R : realFieldType) (f g : (\bar R)^nat) b :
   (b < 0)%R -> f @ \oo --> -oo -> g @ \oo --> b%:E -> f \* g @ \oo --> +oo.
@@ -1876,15 +1852,10 @@ Proof.
 move=> b_lt0 fl gl; have /= := cvgeM _ fl gl; rewrite lt0_mulNye//; apply.
 by rewrite mule_def_infty_neq0// lt_eqF.
 Qed.
-#[deprecated(since="mathcomp-analysis 0.6.0", note="use `cvgeM` instead")]
-Notation ereal_cvgM_lt0_ninfty := __deprecated__ereal_cvgM_lt0_ninfty (only parsing).
 
 Lemma __deprecated__ereal_cvgM (R : realType) (f g : (\bar R) ^nat) (a b : \bar R) :
  a *? b -> f @ \oo --> a -> g @ \oo --> b -> f \* g @ \oo --> a * b.
 Proof. exact: cvgeM. Qed.
-#[deprecated(since="mathcomp-analysis 0.6.0",
-  note="renamed to `cvgeM` and generalized")]
-Notation ereal_cvgM := __deprecated__ereal_cvgM (only parsing).
 
 Lemma __deprecated__ereal_lim_sum (R : realFieldType) (I : Type) (r : seq I)
     (f : I -> (\bar R)^nat) (l : I -> \bar R) (P : pred I) :
@@ -1894,9 +1865,6 @@ Lemma __deprecated__ereal_lim_sum (R : realFieldType) (I : Type) (r : seq I)
 Proof.
 by move=> f0 ?; apply: cvg_nnesum => // ? ?; apply: nearW => ?; apply: f0.
 Qed.
-#[deprecated(since="mathcomp-analysis 0.6.0",
-  note="renamed to `cvg_nnesum` and generalized")]
-Notation ereal_lim_sum := __deprecated__ereal_lim_sum (only parsing).
 
 Let lim_shift_cst (R : realFieldType) (u : (\bar R) ^nat) (l : \bar R) :
     cvgn u -> (forall n, 0 <= u n) -> -oo < l ->
@@ -1995,6 +1963,79 @@ Lemma eseries_mkcond [R : realFieldType] [P : pred nat] (f : nat -> \bar R) :
 Proof. by apply/congr_lim/eq_fun => n /=; apply: big_mkcond. Qed.
 
 End sequences_ereal.
+#[deprecated(since="mathcomp-analysis 0.6.0",
+  note="use `cvgeyPge` or a variant instead")]
+Notation ereal_cvgPpinfty := __deprecated__ereal_cvgPpinfty (only parsing).
+#[deprecated(since="mathcomp-analysis 0.6.0",
+  note="use `cvgeNyPle` or a variant instead")]
+Notation ereal_cvgPninfty := __deprecated__ereal_cvgPninfty (only parsing).
+#[deprecated(since="mathcomp-analysis 0.6.0",
+  note="renamed to `squeeze_cvge` and generalized")]
+Notation ereal_squeeze := __deprecated__ereal_squeeze (only parsing).
+#[deprecated(since="mathcomp-analysis 0.6.0", note="use `cvgeD` instead")]
+Notation ereal_cvgD_pinfty_fin := __deprecated__ereal_cvgD_pinfty_fin (only parsing).
+#[deprecated(since="mathcomp-analysis 0.6.0", note="use `cvgeD` instead")]
+Notation ereal_cvgD_ninfty_fin := __deprecated__ereal_cvgD_ninfty_fin (only parsing).
+#[deprecated(since="mathcomp-analysis 0.6.0", note="use `cvgeD` instead")]
+Notation ereal_cvgD_pinfty_pinfty := __deprecated__ereal_cvgD_pinfty_pinfty (only parsing).
+#[deprecated(since="mathcomp-analysis 0.6.0",
+  note="renamed to `cvgeD` and generalized")]
+Notation ereal_cvgD := __deprecated__ereal_cvgD (only parsing).
+#[deprecated(since="mathcomp-analysis 0.6.0",
+  note="renamed to `cvgeB` and generalized")]
+Notation ereal_cvgB := __deprecated__ereal_cvgB (only parsing).
+#[deprecated(since="mathcomp-analysis 0.6.0",
+  note="renamed to `is_cvgeD` and generalized")]
+Notation ereal_is_cvgD := __deprecated__ereal_is_cvgD (only parsing).
+#[deprecated(since="mathcomp-analysis 0.6.0",
+  note="renamed to `cvge_sub0` and generalized")]
+Notation ereal_cvg_sub0 := __deprecated__ereal_cvg_sub0 (only parsing).
+#[deprecated(since="mathcomp-analysis 0.6.0",
+  note="renamed to `limeD` and generalized")]
+Notation ereal_limD := __deprecated__ereal_limD (only parsing).
+#[deprecated(since="mathcomp-analysis 0.6.0", note="use `cvgeM` instead")]
+Notation ereal_cvgM_gt0_pinfty := __deprecated__ereal_cvgM_gt0_pinfty (only parsing).
+#[deprecated(since="mathcomp-analysis 0.6.0", note="use `cvgeM` instead")]
+Notation ereal_cvgM_lt0_pinfty := __deprecated__ereal_cvgM_lt0_pinfty (only parsing).
+#[deprecated(since="mathcomp-analysis 0.6.0", note="use `cvgeM` instead")]
+Notation ereal_cvgM_gt0_ninfty := __deprecated__ereal_cvgM_gt0_ninfty (only parsing).
+#[deprecated(since="mathcomp-analysis 0.6.0", note="use `cvgeM` instead")]
+Notation ereal_cvgM_lt0_ninfty := __deprecated__ereal_cvgM_lt0_ninfty (only parsing).
+#[deprecated(since="mathcomp-analysis 0.6.0",
+  note="renamed to `cvgeM` and generalized")]
+Notation ereal_cvgM := __deprecated__ereal_cvgM (only parsing).
+#[deprecated(since="mathcomp-analysis 0.6.0",
+  note="renamed to `cvg_nnesum` and generalized")]
+Notation ereal_lim_sum := __deprecated__ereal_lim_sum (only parsing).
+#[deprecated(since="mathcomp-analysis 0.6.0",
+  note="renamed to `cvg_abse0P` and generalized")]
+Notation ereal_cvg_abs0 := __deprecated__ereal_cvg_abs0 (only parsing).
+#[deprecated(since="mathcomp-analysis 0.6.0", note="use `cvge_ge` instead")]
+Notation ereal_cvg_ge0 := __deprecated__ereal_cvg_ge0 (only parsing).
+#[deprecated(since="mathcomp-analysis 0.6.0",
+  note="renamed to `lime_ge` and generalized")]
+Notation ereal_lim_ge := __deprecated__ereal_lim_ge (only parsing).
+#[deprecated(since="mathcomp-analysis 0.6.0",
+  note="renamed to `lime_le` and generalized")]
+Notation ereal_lim_le := __deprecated__ereal_lim_le (only parsing).
+#[deprecated(since="mathcomp-analysis 0.6.0",
+  note="renamed to `cvgeryP` and generalized")]
+Notation dvg_ereal_cvg := __deprecated__dvg_ereal_cvg (only parsing).
+#[deprecated(since="mathcomp-analysis 0.6.0",
+  note="renamed to `fine_cvgP` and generalized")]
+Notation ereal_cvg_real := __deprecated__ereal_cvg_real (only parsing).
+#[deprecated(since="mathcomp-analysis 0.6.6",
+  note="renamed to `ereal_nondecreasing_cvgn`")]
+Notation ereal_nondecreasing_cvg := ereal_nondecreasing_cvgn (only parsing).
+#[deprecated(since="mathcomp-analysis 0.6.6",
+  note="renamed to `ereal_nondecreasing_is_cvgn`")]
+Notation ereal_nondecreasing_is_cvg := ereal_nondecreasing_is_cvgn (only parsing).
+#[deprecated(since="mathcomp-analysis 0.6.6",
+  note="renamed to `ereal_nonincreasing_cvgn`")]
+Notation ereal_nonincreasing_cvg := ereal_nonincreasing_cvgn (only parsing).
+#[deprecated(since="mathcomp-analysis 0.6.6",
+  note="renamed to `ereal_nonincreasing_is_cvgn`")]
+Notation ereal_nonincreasing_is_cvg := ereal_nonincreasing_is_cvgn (only parsing).
 #[deprecated(since="analysis 0.6.0", note="Use eseries0 instead.")]
 Notation nneseries0 := eseries0 (only parsing).
 #[deprecated(since="analysis 0.6.0", note="Use eq_eseriesr instead.")]
@@ -2064,7 +2105,7 @@ Qed.
 Lemma is_cvg_sups u : cvgn u -> cvgn (sups u).
 Proof.
 move=> cf; have [M [Mreal Mu]] := cvg_seq_bounded cf.
-apply: nonincreasing_is_cvg.
+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 ltrDl.
@@ -2089,8 +2130,7 @@ Qed.
 Lemma cvg_sups_inf u : has_ubound (range u) -> has_lbound (range u) ->
   sups u @ \oo --> inf (range (sups u)).
 Proof.
-move=> u_ub u_lb.
-apply: nonincreasing_cvg; first exact: nonincreasing_sups.
+move=> u_ub u_lb; apply: nonincreasing_cvgn; first exact: nonincreasing_sups.
 case: u_lb => M uM; exists M => _ [n _ <-].
 rewrite (@le_trans _ _ (u n)) //; first by apply: uM; exists n.
 by apply: sup_ub; [exact/has_ubound_sdrop|exists n => /=].
@@ -2257,13 +2297,13 @@ move=> ba bb; have ab k : sups (u \+ v) k <= sups u k + sups v k.
     exact/has_ubound_sdrop/bounded_fun_has_ubound; exact | exists n |
     exact/has_ubound_sdrop/bounded_fun_has_ubound; exact | exists n ].
 have cu : cvgn (sups u).
-  apply: nonincreasing_is_cvg; last exact: bounded_fun_has_lbound_sups.
+  apply: nonincreasing_is_cvgn; last exact: bounded_fun_has_lbound_sups.
   exact/nonincreasing_sups/bounded_fun_has_ubound.
 have cv : cvgn (sups v).
-  apply: nonincreasing_is_cvg; last exact: bounded_fun_has_lbound_sups.
+  apply: nonincreasing_is_cvgn; last exact: bounded_fun_has_lbound_sups.
   exact/nonincreasing_sups/bounded_fun_has_ubound.
 rewrite -(limD cu cv); apply: ler_lim.
-- apply: nonincreasing_is_cvg; last first.
+- apply: nonincreasing_is_cvgn; last first.
     exact/bounded_fun_has_lbound_sups/bounded_funD.
   exact/nonincreasing_sups/bounded_fun_has_ubound/bounded_funD.
 - exact: is_cvgD cu cv.
@@ -2279,14 +2319,14 @@ move=> ba bb; have ab k : infs u k + infs v k <= infs (u \+ v) k.
     exact/has_lbound_sdrop/bounded_fun_has_lbound; exact | exists n |
     exact/has_lbound_sdrop/bounded_fun_has_lbound; exact | exists n ].
 have cu : cvgn (infs u).
-  apply: nondecreasing_is_cvg; last exact: bounded_fun_has_ubound_infs.
+  apply: nondecreasing_is_cvgn; last exact: bounded_fun_has_ubound_infs.
   exact/nondecreasing_infs/bounded_fun_has_lbound.
 have cv : cvgn (infs v).
-  apply: nondecreasing_is_cvg; last exact: bounded_fun_has_ubound_infs.
+  apply: nondecreasing_is_cvgn; last exact: bounded_fun_has_ubound_infs.
   exact/nondecreasing_infs/bounded_fun_has_lbound.
 rewrite -(limD cu cv); apply: ler_lim.
 - exact: is_cvgD cu cv.
-- apply: nondecreasing_is_cvg; last first.
+- apply: nondecreasing_is_cvgn; last first.
     exact/bounded_fun_has_ubound_infs/bounded_funD.
   exact/nondecreasing_infs/bounded_fun_has_lbound/bounded_funD.
 - exact: nearW.
@@ -2382,13 +2422,13 @@ by rewrite (@le_trans _ _ a) //; [exact/ereal_inf_lb|exact/ereal_sup_ub].
 Unshelve. all: by end_near. Qed.
 
 Lemma cvg_esups_inf u : esups u @ \oo --> ereal_inf (range (esups u)).
-Proof. by apply: ereal_nonincreasing_cvg => //; exact: nonincreasing_esups. Qed.
+Proof. by apply: ereal_nonincreasing_cvgn => //; exact: nonincreasing_esups. Qed.
 
 Lemma is_cvg_esups u : cvgn (esups u).
 Proof. by apply/cvg_ex; eexists; exact/cvg_esups_inf. Qed.
 
 Lemma cvg_einfs_sup u : einfs u @ \oo --> ereal_sup (range (einfs u)).
-Proof. by apply: ereal_nondecreasing_cvg => //; exact: nondecreasing_einfs. Qed.
+Proof. by apply: ereal_nondecreasing_cvgn => //; exact: nondecreasing_einfs. Qed.
 
 Lemma is_cvg_einfs u : cvgn (einfs u).
 Proof. by apply/cvg_ex; eexists; exact/cvg_einfs_sup. Qed.
@@ -2583,7 +2623,7 @@ Proof.
 move=> a0 x0 x1.
 have /(@cvg_unique _ (@Rhausdorff R)) := @cvg_geometric_series _ a _ x1.
 move/(_ _ (@is_cvg_geometric_series _ a _ x1)) => ->.
-apply: nondecreasing_cvg_le; last exact: is_cvg_geometric_series.
+apply: nondecreasing_cvgn_le; last exact: is_cvg_geometric_series.
 by apply: nondecreasing_series => ? _ /=; rewrite pmulr_lge0 // exprn_gt0.
 Qed.