diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 67bb43c3b6..9fb57d4ec6 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -4,6 +4,13 @@
 
 ### Added
 
+- in `pseudometric_normed_Zmodule.v`:
+  + lemmas `cvg0D`, `cvgD0`, `cvg0B`, `cvgB0`, `cvgN0`
+
+- in `normed_module.v`:
+  + lemmas `cvg1M`, `cvgM1`, `cvg0M`, `cvgM0`
+  + lemmas `cvg1Z`, `cvg0Z`, `cvgZ0`
+
 ### Changed
 
 ### Renamed
diff --git a/theories/derive.v b/theories/derive.v
index b3727b1587..33b99954aa 100644
--- a/theories/derive.v
+++ b/theories/derive.v
@@ -403,8 +403,8 @@ evar (g : R -> W); rewrite [X in X @ _](_ : _ = g) /=.
 apply: cvg_lim => //.
 pose g1 : R -> W := fun h => (h^-1 * h) *: 'd f a v.
 pose g2 : R -> W := fun h : R => h^-1 *: k (h *: v ).
-rewrite (_ : g = g1 + g2) ?funeqE // -(addr0 (_ _ v)); apply: cvgD.
-  rewrite -(scale1r (_ _ v)); apply: cvgZr_tmp => /= X [e e0].
+rewrite (_ : g = g1 + g2) ?funeqE//; apply: cvgD0.
+  apply: cvg1Z => //= X [e e0].
   rewrite /ball_ /= => eX.
   apply/nbhs_ballP.
   by exists e => //= x _ x0; apply eX; rewrite mulVf//= subrr normr0.
@@ -431,8 +431,8 @@ Qed.
 End DifferentialR_numFieldType.
 
 Section DifferentialR2.
-Variable R : numFieldType.
-Implicit Type (V : normedModType R).
+Context {R : numFieldType}.
+Implicit Type V : normedModType R.
 
 Lemma deriveEjacobian m n (f : 'rV[R]_m -> 'rV[R]_n) (a v : 'rV[R]_m) :
   differentiable f a -> 'D_ v f a = v *m jacobian f a.
@@ -1198,7 +1198,7 @@ End DeriveVW.
 Arguments derivable_cst {R V W}.
 
 Section Derive_lemmasVW.
-Variables (R : numFieldType) (V W : normedModType R).
+Context {R : numFieldType} {V W : normedModType R}.
 Implicit Types f g : V -> W.
 
 Fact der_add f g (x v : V) : derivable f x v -> derivable g x v ->
@@ -1206,9 +1206,10 @@ Fact der_add f g (x v : V) : derivable f x v -> derivable g x v ->
   0^'  --> 'D_v f x + 'D_v g x.
 Proof.
 move=> df dg.
-evar (fg : R -> W); rewrite [X in X @ _](_ : _ = fg) /=.
-  rewrite funeqE => h.
-  by rewrite !scalerDr scalerN scalerDr opprD addrACA -!scalerBr /fg.
+under [X in X @ _]eq_fun.
+  move=> /= h.
+  rewrite !scalerDr scalerN scalerDr opprD addrACA -!scalerBr.
+  over.
 exact: cvgD.
 Qed.
 
@@ -1537,7 +1538,7 @@ pose g t : R := (sup (f @` A) - f t)^-1.
 have invf_continuous : {within A, continuous g}.
   rewrite continuous_subspace_in => t tA; apply: cvgV => //=.
     by rewrite subr_eq0 gt_eqF// AfsupfA//; rewrite inE in tA.
-  by apply: cvgD; [exact: cst_continuous | apply: cvgN; exact: cf].
+  by apply: cvgD => //; apply: cvgN; exact: cf.
 have /ex_strict_bound_gt0[k k_gt0 /= imVfltk] : bounded_set (g @` A).
   exact/compact_bounded/continuous_compact.
 have [_ [t tA <-]] : exists2 y, (f @` A) y & sup (f @` A) - k^-1 < y.
@@ -2211,9 +2212,7 @@ move=> fx_lt_gx fg_neq df dg cf cg; case: ifPn => fg /=.
         h (shift x (k *: v)) @[k --> nbhs 0^'] --> h x.
       move=> ch.
       apply: cvg_comp; last exact: ch.
-      rewrite -[in nbhs x](add0r x); apply: cvgD => //.
-      rewrite -(scale0r v); apply: cvgZ => //.
-      exact: nbhs_dnbhs.
+      by apply: cvg0D => //; apply: cvg0Z => //; exact: nbhs_dnbhs.
     apply/(cvgr_lt (f x - g x)); last by rewrite subr_lt0.
     by apply: cvgB; exact: Hf.
   + exact: dg.
diff --git a/theories/gauss_integral.v b/theories/gauss_integral.v
index aa8ab15355..acaf3b7bec 100644
--- a/theories/gauss_integral.v
+++ b/theories/gauss_integral.v
@@ -1,4 +1,4 @@
-(* mathcomp analysis (c) 2025 Inria and AIST. License: CeCILL-C.              *)
+(* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C.              *)
 From HB Require Import structures.
 From mathcomp Require Import boot order ssralg ssrnum ssrint interval.
 From mathcomp Require Import finmap.
@@ -49,9 +49,7 @@ Proof. by apply: measurableT_comp => //; exact: measurableT_comp. Qed.
 Lemma continuous_gauss_fun : continuous gauss_fun.
 Proof.
 move=> x; apply: (@continuous_comp _ _ _ (fun x : R => - x ^+ 2) expR).
-  apply: cvgN; apply: (cvg_comp (fun z => z) (fun z => z ^+ 2)).
-    exact: cvg_id.
-  exact: exprn_continuous.
+  by apply: cvgN; exact: exprn_continuous.
 exact: continuous_expR.
 Qed.
 
@@ -331,15 +329,14 @@ have h_h0 x : 0 < x -> h x = h 0.
       under [X in X @ _ --> _]eq_fun do rewrite expr2.
       by apply: cvgM; apply: continuous_integral0_gauss; exact: ltW.
     by apply: derivable_within_continuous => u _; exact: derivable_integral01_u.
-  move=> c; rewrite in_itv/= => /andP[c0 cx].
-  by rewrite derive_h// mul0r => /eqP; rewrite subr_eq0 => /eqP.
+  by move=> c c0x; rewrite derive_h ?(itvP c0x)// mul0r => /subr0_eq.
 have Ig2 x : 0 < x -> (integral0_gauss x) ^+ 2 = pi / 4 - integral01_u x.
   move/h_h0/eqP; rewrite {1}/h eq_sym addrC -subr_eq => /eqP/esym.
   by rewrite h0.
 suff: pi / 4 - integral01_u x @[x --> +oo] --> pi / 4.
   apply: cvg_trans; apply: near_eq_cvg.
   by near=> x; rewrite Ig2.
-by rewrite -[in X in _ --> X](subr0 (pi / 4)); exact: cvgB.
+exact: cvgB0.
 Unshelve. end_near. Qed.
 
 End gauss_integral_proof.
diff --git a/theories/normedtype_theory/normed_module.v b/theories/normedtype_theory/normed_module.v
index 1ce82b902d..706671a82a 100644
--- a/theories/normedtype_theory/normed_module.v
+++ b/theories/normedtype_theory/normed_module.v
@@ -569,17 +569,15 @@ Unshelve. all: by end_near. Qed.
 End NVS_continuity_mul.
 
 Section cvg_composition_normed.
-Context {K : numFieldType} {V : normedModType K} {T : Type}.
-Context (F : set_system T) {FF : Filter F}.
+Context {K : numFieldType} {V : normedModType K} {T : Type}
+  (F : set_system T) {FF : Filter F}.
 Implicit Types (f g : T -> V) (s : T -> K) (k : K) (x : T) (a b : V).
 
 Lemma cvgZ s f k a : s @ F --> k -> f @ F --> a ->
                      s x *: f x @[x --> F] --> k *: a.
 Proof.
 move=> ? ?; apply: continuous2_cvg => //.
-have := (@scale_continuous K V (k, a)).
-rewrite /continuous_at/=.
-exact.
+exact: (@scale_continuous K V (k, a)).
 Qed.
 
 Lemma is_cvgZ s f : cvg (s @ F) ->
@@ -589,6 +587,15 @@ Proof. by have := cvgP _ (cvgZ _ _); apply. Qed.
 Lemma cvgZr_tmp s k a : s @ F --> k -> s x *: a @[x --> F] --> k *: a.
 Proof. by move=> ?; exact: cvgZ. Qed.
 
+Lemma cvg1Z s f a : s @ F --> (1 : K) -> f @ F --> a -> s x *: f x @[x --> F] --> a.
+Proof. by move=> /cvgZ /[apply]; rewrite scale1r. Qed.
+
+Lemma cvg0Z s f a : s @ F --> (0 : K) -> f @ F --> a -> s x *: f x @[x --> F] --> 0.
+Proof. by move=> /cvgZ /[apply]; rewrite scale0r. Qed.
+
+Lemma cvgZ0 s f k : s @ F --> k -> f @ F --> (0 : V) -> s x *: f x @[x --> F] --> 0.
+Proof. by move=> /cvgZ /[apply]; rewrite scaler0. Qed.
+
 Lemma is_cvgZr_tmp s a : cvg (s @ F) -> cvg ((fun x => s x *: a) @ F).
 Proof. by have := cvgP _ (cvgZr_tmp  _); apply. Qed.
 
@@ -600,8 +607,9 @@ Proof. by have := cvgP _ (cvgZl_tmp  _); apply. Qed.
 
 Lemma is_cvgZlE k f : k != 0 -> cvg (k *: f @ F) = cvg (f @ F).
 Proof.
-move=> k_neq0; rewrite propeqE; split => [/(@cvgZl_tmp k^-1)|/(@cvgZl_tmp k)/cvgP//].
-by under [_ \*: _]funext => x /= do rewrite scalerK//; apply: cvgP.
+move=> k_neq0.
+rewrite propeqE; split => [/(@cvgZl_tmp k^-1)|/(@cvgZl_tmp k)/cvgP//].
+by under [_ \*: _]funext => x /= do rewrite scalerK//; exact: cvgP.
 Qed.
 
 End cvg_composition_normed.
@@ -623,8 +631,7 @@ Notation is_cvgZr := is_cvgZl_tmp (only parsing).
 Notation is_cvgZrE := is_cvgZlE (only parsing).
 
 Section cvg_composition_field.
-Context {K : numFieldType}  {T : Type}.
-Context (F : set_system T) {FF : Filter F}.
+Context {K : numFieldType} {T : Type} (F : set_system T) {FF : Filter F}.
 Implicit Types (f g : T -> K) (a b : K).
 
 Lemma cvgV f a : a != 0 -> f @ F --> a -> f\^-1 @ F --> a^-1.
@@ -650,6 +657,18 @@ Proof. exact: cvgZr_tmp. Qed.
 Lemma cvgMl_tmp g a b : g @ F --> b -> a * g x @[x --> F] --> a * b.
 Proof. exact: cvgZl_tmp. Qed.
 
+Lemma cvg1M f g a : f @ F --> (1 :> K) -> g @ F --> a -> f \* g @ F --> a.
+Proof. by move=> /cvgM /[apply]; rewrite mul1r. Qed.
+
+Lemma cvgM1 f g a : f @ F --> a -> g @ F --> (1 :> K) -> f \* g @ F --> a.
+Proof. by move=> /cvgM /[apply]; rewrite mulr1. Qed.
+
+Lemma cvg0M f g a : f @ F --> 0 -> g @ F --> a -> f \* g @ F --> 0.
+Proof. by move=> /cvgM /[apply]; rewrite mul0r. Qed.
+
+Lemma cvgM0 f g a : f @ F --> a -> g @ F --> 0 -> f \* g @ F --> 0.
+Proof. by move=> /cvgM /[apply]; rewrite mulr0. Qed.
+
 Lemma is_cvgM f g : cvg (f @ F) -> cvg (g @ F) -> cvg (f \* g @ F).
 Proof. exact: is_cvgZ. Qed.
 
@@ -783,17 +802,17 @@ Proof. by move=> ?; apply: cvgN. Qed.
 Lemma continuousD f g x :
   {for x, continuous f} -> {for x, continuous g} ->
   {for x, continuous (f + g)}.
-Proof. by move=> f_cont g_cont; apply: cvgD. Qed.
+Proof. by move=> ? ?; exact: cvgD. Qed.
 
 Lemma continuousB f g x :
   {for x, continuous f} -> {for x, continuous g} ->
   {for x, continuous (f - g)}.
-Proof. by move=> f_cont g_cont; apply: cvgB. Qed.
+Proof. by move=> ? ?; exact: cvgB. Qed.
 
 Lemma continuousZ s f x :
   {for x, continuous s} -> {for x, continuous f} ->
   {for x, continuous (fun x => s x *: f x)}.
-Proof. by move=> ? ?; apply: cvgZ. Qed.
+Proof. by move=> ? ?; exact: cvgZ. Qed.
 
 Lemma continuousZl_tmp f k x :
   {for x, continuous f} -> {for x, continuous (k \*: f)}.
@@ -806,11 +825,11 @@ Proof. by move=> ?; exact: cvgZr_tmp. Qed.
 Lemma continuousM s t x :
   {for x, continuous s} -> {for x, continuous t} ->
   {for x, continuous (s \* t)}.
-Proof. by move=> f_cont g_cont; exact: cvgM. Qed.
+Proof. by move=> ? ?; exact: cvgM. Qed.
 
 Lemma continuousV s x : s x != 0 ->
   {for x, continuous s} -> {for x, continuous (fun x => (s x)^-1%R)}.
-Proof. by move=> ?; apply: cvgV. Qed.
+Proof. by move=> ?; exact: cvgV. Qed.
 
 End local_continuity.
 #[deprecated(since="mathcomp-analysis 1.12.0", note="renamed to `continuousZl_tmp`")]
diff --git a/theories/normedtype_theory/pseudometric_normed_Zmodule.v b/theories/normedtype_theory/pseudometric_normed_Zmodule.v
index 5f5260e622..b1f779a5dc 100644
--- a/theories/normedtype_theory/pseudometric_normed_Zmodule.v
+++ b/theories/normedtype_theory/pseudometric_normed_Zmodule.v
@@ -1161,6 +1161,21 @@ Qed.
 Lemma is_cvgDrE f g : cvg (f @ F) -> cvg ((f + g) @ F) = cvg (g @ F).
 Proof. by rewrite addrC; apply: is_cvgDlE. Qed.
 
+Lemma cvg0D f g a : f @ F --> 0 -> g @ F --> a -> f x + g x @[x --> F] --> a.
+Proof. by move=> /cvgD /[apply]; rewrite add0r. Qed.
+
+Lemma cvgD0 f g a : f @ F --> a -> g @ F --> 0 -> f x + g x @[x --> F] --> a.
+Proof. by move=> /cvgD /[apply]; rewrite addr0. Qed.
+
+Lemma cvg0B f g a : f @ F --> 0 -> g @ F --> a -> f x - g x @[x --> F] --> -a.
+Proof. by move=> /cvgB /[apply]; rewrite add0r. Qed.
+
+Lemma cvgB0 f g a : f @ F --> a -> g @ F --> 0 -> f x - g x @[x --> F] --> a.
+Proof. by move=> /cvgB /[apply]; rewrite subr0. Qed.
+
+Lemma cvgN0 f : f @ F --> 0 -> - f @ F --> 0.
+Proof. by rewrite -{2}oppr0; exact: cvgN. Qed.
+
 Lemma cvg_sub0 f g a : (f - g) @ F --> (0 : V) -> g @ F --> a -> f @ F --> a.
 Proof.
 by move=> Cfg Cg; have := cvgD Cfg Cg; rewrite subrK add0r; apply.
diff --git a/theories/normedtype_theory/tvs.v b/theories/normedtype_theory/tvs.v
index 2e29fa236d..79719f209c 100644
--- a/theories/normedtype_theory/tvs.v
+++ b/theories/normedtype_theory/tvs.v
@@ -187,7 +187,7 @@ move=> x; rewrite /continuous_at.
 rewrite -(@eq_cvg _ _ _ (fun x => 0 - x)); first by move=> y; exact: add0r.
 rewrite -[- x]add0r.
 apply: (@continuous_comp _ _ _ (fun x => (0, x)) (fun x : M * M => x.1 - x.2)).
-  by apply: cvg_pair => /=; [exact: cvg_cst|exact: cvg_id].
+  exact: cvg_pair.
 exact: sub_continuous.
 Qed.
 
diff --git a/theories/probability_theory/beta_distribution.v b/theories/probability_theory/beta_distribution.v
index c0b98696a5..1573d70805 100644
--- a/theories/probability_theory/beta_distribution.v
+++ b/theories/probability_theory/beta_distribution.v
@@ -67,7 +67,7 @@ split.
 - by move=> y y01; apply: derivableM => //=; exact: onemXn_derivable.
 - apply: cvgM => //.
   apply: cvg_at_right_filter; apply: (@cvg_comp _ _ _ onem (fun x => x ^+ n)).
-    by apply: cvgB; [exact: cvg_cst|exact: cvg_id].
+    by apply: cvgB; [apply: cvg_cst|apply: cvg_id].
   exact: exprn_continuous.
 - apply: cvg_at_left_filter; apply: cvgM => //.
   apply: (@cvg_comp _ _ _ onem (fun x => x ^+ n)).
diff --git a/theories/probability_theory/random_variable.v b/theories/probability_theory/random_variable.v
index 983d434e19..21e41523b0 100644
--- a/theories/probability_theory/random_variable.v
+++ b/theories/probability_theory/random_variable.v
@@ -350,10 +350,10 @@ have cdf_s : cdf X r @[r --> a^'+] --> s%:E.
     by rewrite (lt_le_trans (ltNyr 0%R)) ?le_ereal_inf_tmp//= => l[? _] <-.
   rewrite (le_lt_trans _ (ltry 1%R))// ge_ereal_inf//=.
   exists (cdf X (a + 1)); last exact: cdf_le1.
-  by exists (a + 1)%R => //; rewrite in_itv /=; apply/andP; rewrite ltrDl.
+  by exists (a + 1)%R => //; rewrite in_itv/= ltrDl// ltr01/=.
 have cdf_ns : cdf X (a + n.+1%:R^-1) @[n --> \oo] --> s%:E.
   move/cvge_at_rightP : cdf_s; apply; split=> [n|]; rewrite ?ltrDl //.
-  rewrite -[X in _ --> X]addr0; apply: cvgD => //.
+  apply: cvgD0 => //.
   by rewrite gtr0_cvgV0 ?cvg_shiftS; [near=> n | exact: cvgr_idn].
 have cdf_na : cdf X (a + n.+1%:R^-1) @[n --> \oo] --> cdf X a.
   pose F n := X @^-1` `]-oo, (a + n.+1%:R^-1)%R].
diff --git a/theories/realfun.v b/theories/realfun.v
index c2e7b6a7b8..1ee878c7f0 100644
--- a/theories/realfun.v
+++ b/theories/realfun.v
@@ -466,7 +466,7 @@ move=> nif; have ndNf : {in `[a, b] &, nondecreasing_fun (-%R \o f)}.
   by move=> x y xab yab xy /=; rewrite lerNl opprK nif.
 move/nondecreasing_at_left_at_right : (ndNf) => H x.
 rewrite in_itv/= => /andP[ax xb]; rewrite -[leLHS]opprK lerNl -!limN//.
-- rewrite -(opprK f);apply: is_cvgN.
+- rewrite -(opprK f); apply: is_cvgN.
   exact: nondecreasing_at_left_is_cvgrW ndNf.
 - rewrite -(opprK f); apply: is_cvgN.
   exact: nondecreasing_at_right_is_cvgrW ndNf.
@@ -2301,11 +2301,11 @@ suff /near_eq_cvg/cvg_trans : {near (- x)^'+,
 apply: filter_app (nbhs_right_lt xa).
 apply: (filter_app _ _ (nbhs_right_ge _)).
 near=> t => xt ta; have ? : -b <= t by exact: (le_trans bx).
-have ? : t <= -a by exact: ltW.
+have ? : t <= - a by exact: ltW.
 apply/eqP; rewrite eq_sym -subr_eq opprK addrC.
 rewrite /= [TV a _ f]total_variation_opp opprK -fineD.
-- by apply/bounded_variationP => //; apply: bounded_variationl bvNf.
-- by apply/bounded_variationP => //; apply: bounded_variationr bvNf.
+- by apply/bounded_variationP => //; exact: bounded_variationl bvNf.
+- by apply/bounded_variationP => //; exact: bounded_variationr bvNf.
 by rewrite -total_variationD.
 Unshelve. all: by end_near. Qed.
 
@@ -2723,8 +2723,7 @@ have f0g0 y : a < y -> y < b ->
     (f0 x - f0 y) / (g0 x - g0 y) @[x --> a^'+] --> f0 y / g0 y.
   move=> ay yb; rewrite -[X in _ --> X]opprK -mulrN -invrN -mulNr.
   apply: cvgM.
-    rewrite -[X in _ --> X]add0r; apply: cvgB => //.
-    apply: cvg_trans fa0; apply: near_eq_cvg; near=> z.
+    apply: cvg0B => //; apply: cvg_trans fa0; apply: near_eq_cvg; near=> z.
     by rewrite /f0 gt_eqF.
   apply: cvgV.
     rewrite oppr_eq0; apply/eqP => g0y0.
@@ -2736,8 +2735,7 @@ have f0g0 y : a < y -> y < b ->
     rewrite mulf_eq0// orbC gt_eqF ?subr_gt0//= => /eqP; apply/eqP.
     apply: cdg.
     by move: c0 c0ay; apply: subset_itvSoo; rewrite bnd_simp// ltW.
-  rewrite -[X in _ --> X]add0r; apply: cvgB => //.
-  apply: cvg_trans ga0; apply: near_eq_cvg; near=> z.
+  apply: cvg0B => //; apply: cvg_trans ga0; apply: near_eq_cvg; near=> z.
   by rewrite /g0 gt_eqF.
 have lfg_ub q : l < q ->
     exists2 c2, a < c2 & forall x, a < x < c2 -> f x / g x < q.
diff --git a/theories/sequences.v b/theories/sequences.v
index f44a62f3d8..fff6e799e9 100644
--- a/theories/sequences.v
+++ b/theories/sequences.v
@@ -247,7 +247,7 @@ Local Notation eqolimPn := (@eqolimP _ _ _ eventually_filter).
 (** Sequences of sets *)
 
 Section seqDU.
-Variables (T : Type).
+Context {T : Type}.
 Implicit Types F : (set T)^nat.
 
 Lemma bigsetU_seqDU F n :
@@ -557,7 +557,7 @@ Lemma eq_sum_telescope (V : zmodType) (u_ : V ^nat) n :
 Proof. by rewrite telescopeK/= addrC addrNK. Qed.
 
 Section series_patched.
-Variables (N : nat) (K : numFieldType) (V : normedModType K).
+Context (N : nat) {K : numFieldType} {V : normedModType K}.
 Implicit Types (f : nat -> V) (u : V ^nat)  (l : set_system V).
 
 Lemma is_cvg_series_restrict u_ :
@@ -574,7 +574,7 @@ Qed.
 End series_patched.
 
 Section sequences_R_lemmas.
-Variable R : realType.
+Context {R : realType}.
 
 Lemma nondecreasing_cvgn (u_ : R ^nat) :
     nondecreasing_seq u_ -> has_ubound (range u_) ->
@@ -746,7 +746,7 @@ Unshelve. all: by end_near. Qed.
 End cesaro.
 
 Section cesaro_converse.
-Variable R : archiRealFieldType.
+Context {R : archiRealFieldType}.
 
 Let cesaro_converse_off_by_one (u_ : R ^nat) :
     [sequence n.+1%:R^-1 * series u_ n.+1]_n @ \oo --> 0 ->
@@ -771,10 +771,9 @@ pose a_ := telescope u_ => a_o u_l.
 suff abel : forall n,
     u_ n - arithmetic_mean u_ n = \sum_(1 <= k < n.+1) k%:R / n.+1%:R * a_ k.-1.
   suff K : u_ - arithmetic_mean u_ @ \oo --> 0.
-    rewrite -(add0r l).
     rewrite (_ : u_ = u_ - arithmetic_mean u_ + arithmetic_mean u_).
       by rewrite funeqE => n; rewrite subrK.
-    exact: cvgD.
+    exact: cvg0D.
   rewrite (_ : _ - arithmetic_mean u_ =
       (fun n => \sum_(1 <= k < n.+1) k%:R / n.+1%:R * a_ k.-1)).
     by rewrite funeqE.
@@ -913,15 +912,14 @@ rewrite seriesEnat !mulrBr [in LHS]mulr1 mulr_suml -opprB -sumrB.
 by under eq_bigr do rewrite -mulrA -exprSr; rewrite telescope_sumr// opprB.
 Qed.
 
-Lemma cvg_geometric_series (R : archiRealFieldType) (a z : R) : `|z| < 1 ->
-  series (geometric a z) @ \oo --> (a * (1 - z)^-1).
+Lemma cvg_geometric_series {R : archiRealFieldType} (a z : R) : `|z| < 1 ->
+  series (geometric a z) @ \oo --> a * (1 - z)^-1.
 Proof.
 move=> Nz_lt1; rewrite geometric_seriesE ?lt_eqF 1?ltr_normlW//.
-have -> : a / (1 - z) = (a * (1 - 0)) / (1 - z) by rewrite subr0 mulr1.
-by apply: cvgMr_tmp; apply: cvgMl_tmp; apply: cvgB => //; exact: cvg_expr.
+by apply: cvgMr_tmp; apply: cvgM1 => //; apply: cvgB0 => //; exact: cvg_expr.
 Qed.
 
-Lemma cvg_geometric_series_half (R : archiRealFieldType) (r : R) n :
+Lemma cvg_geometric_series_half {R : archiRealFieldType} (r : R) n :
   series (fun k => r / (2 ^ (k + n.+1))%:R : R^o) @ \oo --> (r / 2 ^+ n : R^o).
 Proof.
 rewrite (_ : series _ = series (geometric (r / (2 ^ n.+1)%:R) 2^-1%R)).
@@ -2393,14 +2391,14 @@ Lemma limn_infD u v : cvgn u -> cvgn v ->
 Proof.
 move=> cu cv; rewrite (cvg_limn_infE cu) -(cvg_limn_supE cu).
 rewrite (cvg_limn_infE cv) -(cvg_limn_supE cv) -limn_supD//.
-rewrite cvg_limn_supE; first exact: (@is_cvgD _ _ _ _ _ _ _ cu cv).
-by rewrite cvg_limn_infE //; exact: (@is_cvgD _ _ _ _ _ _ _ cu cv).
+rewrite cvg_limn_supE; first exact: is_cvgD cu cv.
+by rewrite cvg_limn_infE //; exact: is_cvgD cu cv.
 Qed.
 
 End limn_sup_limn_inf.
 
 Section esups_einfs.
-Variable R : realType.
+Context {R : realType}.
 Implicit Types (u : (\bar R)^nat).
 Local Open Scope ereal_scope.