diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index abfeca0128..cb713326bd 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -243,6 +243,7 @@
     `within_continuousMl`, and `within_continuousMr`
 - in `pseudometric_normed_Zmodule.v`
   + new lemma `within_continuousN`
+
 - in `lebesgue_stieltjes_measure.v`:
   + module `MeasurableRocitv`
   + definition `open_type`
@@ -260,6 +261,13 @@
 - in `real_interval.v`:
   + lemma `set1_bigcap_oo`
 
+- in `normed_module.v`,
+  + new lemmas `cvg1MC`, `cvg1M`, `cvgCM1`, `cvgM1`, `cvg0MC`, `cvg0M`, 
+    `cvgCM0`, and `cvgM0`.
+- in `pseudometric_normed_Zmodule.v`,
+  + new lemmas `cvgDl`, `cvgDr`, `cvgBl`, `cvgBr`, `cvg0D`, `cvg0DC`, 
+    `cvgD0`, `cvgCD0`, `cvg0B`, `cvg0BC`, `cvgB0`, `cvgCB0`, and `cvgN0`.
+
 ### Changed
 
 - in `realsum.v`:
diff --git a/theories/normedtype_theory/normed_module.v b/theories/normedtype_theory/normed_module.v
index 80e2cc4f9d..f93157a5b0 100644
--- a/theories/normedtype_theory/normed_module.v
+++ b/theories/normedtype_theory/normed_module.v
@@ -648,6 +648,30 @@ 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 cvg1MC f a : f @ F --> (1 :> K) -> f x * a @[x --> F] --> a.
+Proof. by move/(cvgMr_tmp (b := a)); rewrite mul1r. 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 cvgCM1 f a : f @ F --> (1 :> K) -> a * f x @[x --> F] --> a.
+Proof. by move/(cvgMl_tmp (a := a)); rewrite mulr1. 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 cvg0MC f a : f @ F --> 0 -> f x * a @[x --> F] --> 0.
+Proof. by move/(cvgMr_tmp (b := a)); rewrite mul0r. 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 cvgCM0 f a : f @ F --> 0 -> a * f x @[x --> F] --> 0.
+Proof. by move/(cvgMl_tmp (a := a)); rewrite mulr0. 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.
 
diff --git a/theories/normedtype_theory/pseudometric_normed_Zmodule.v b/theories/normedtype_theory/pseudometric_normed_Zmodule.v
index 920f434388..ce5cdf293b 100644
--- a/theories/normedtype_theory/pseudometric_normed_Zmodule.v
+++ b/theories/normedtype_theory/pseudometric_normed_Zmodule.v
@@ -1098,6 +1098,45 @@ 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 cvgDl f a b : f @ F --> b -> a + f x @[x --> F] --> a + b.
+Proof. apply: cvgD; exact: cvg_cst. Qed.
+
+Lemma cvgDr f a b : f @ F --> a -> f x + b @[x --> F] --> a + b.
+Proof. move/cvgD; apply; exact: cvg_cst. Qed.
+
+Lemma cvgBl f a b : f @ F --> b -> a - f x @[x --> F] --> a - b.
+Proof. by move/cvgN; apply: cvgDl. Qed.
+
+Lemma cvgBr f a b : f @ F --> a -> f x - b @[x --> F] --> a - b.
+Proof. exact: cvgDr. 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 cvg0DC f a : f @ F --> 0 -> f x + a @[x --> F] --> a.
+Proof. by move=> /(cvgDr (b := a)); 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 cvgCD0 f a : f @ F --> 0 -> a + f x @[x --> F] --> a.
+Proof. by move/(@cvgDl _ a); 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 cvg0BC f a : f @ F --> 0 -> f x - a @[x --> F] --> -a.
+Proof. by move=> /(cvgBr (b := a)); 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 cvgCB0 f a : f @ F --> 0 -> a - f x @[x --> F] --> a.
+Proof. by move/(@cvgBl _ a); 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.