rename lemmas

Author: amolinamounier

CHANGELOG_UNRELEASED.md

@@ -273,11 +273,11 @@
     `dsnd_dswap`, `dsndE`, `pr_dlet` are no longer deprecated
 
 - in `normed_module.v`:
-  + lemmas `cvg1MC`, `cvg1M`, `cvgCM1`, `cvgM1`, `cvg0MC`, `cvg0M`,
-    `cvgCM0`, and `cvgM0`
+  + lemmas `cvg1Mcst`, `cvg1M`, `cvgcstM1`, `cvgM1`, `cvg0Mcst`, `cvg0M`,
+    `cvgcstM0`, and `cvgM0`
 - in `pseudometric_normed_Zmodule.v`:
-  + lemmas `cvg0D`, `cvg0DC`,
-    `cvgD0`, `cvgCD0`, `cvg0B`, `cvg0BC`, `cvgB0`, `cvgCB0`, and `cvgN0`
+  + lemmas `cvg0D`, `cvg0Dcst`,
+    `cvgD0`, `cvgcstD0`, `cvg0B`, `cvg0Bcst`, `cvgB0`, `cvgcstB0`, and `cvgN0`
 
 ### Changed
 

theories/normedtype_theory/normed_module.v

@@ -648,25 +648,25 @@ 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.
+Lemma cvg1Mcst f a : f @ F --> (1 :> K) -> f x * a @[x --> F] --> a.
 Proof. by move/(@cvgMr_tmp _ _ 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.
+Lemma cvgcstM1 f a : f @ F --> (1 :> K) -> a * f x @[x --> F] --> a.
 Proof. by move/(@cvgMl_tmp _ 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.
+Lemma cvg0Mcst f a : f @ F --> 0 -> f x * a @[x --> F] --> 0.
 Proof. by move/(@cvgMr_tmp _ _ 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.
+Lemma cvgcstM0 f a : f @ F --> 0 -> a * f x @[x --> F] --> 0.
 Proof. by move/(@cvgMl_tmp _ a); rewrite mulr0. Qed.
 
 Lemma cvgM0 f g a : f @ F --> a -> g @ F --> 0 -> f \* g @ F --> 0.

theories/normedtype_theory/pseudometric_normed_Zmodule.v

@@ -1101,25 +1101,25 @@ 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 cvg0DC f a : f @ F --> 0 -> f x + a @[x --> F] --> a.
+Lemma cvg0Dcst f a : f @ F --> 0 -> f x + a @[x --> F] --> a.
 Proof. by move=> ?; rewrite -[X in _ --> X]add0r; exact: cvgD. 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.
+Lemma cvgcstD0 f a : f @ F --> 0 -> a + f x @[x --> F] --> a.
 Proof. by move=> ?; rewrite -[X in _ --> X]addr0; exact: cvgD. 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.
+Lemma cvg0Bcst f a : f @ F --> 0 -> f x - a @[x --> F] --> - a.
 Proof. by move=> ?; rewrite -[X in _ --> X]sub0r; exact: cvgB. 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.
+Lemma cvgcstB0 f a : f @ F --> 0 -> a - f x @[x --> F] --> a.
 Proof. by move=> ?; rewrite -[X in _ --> X]subr0; exact: cvgB. Qed.
 
 Lemma cvgN0 f : f @ F --> 0 -> - f @ F --> 0.