fix naming

2 files changed, 14 insertions, 14 deletions

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index a5fae21..20594ab 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -12,8 +12,8 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/).
 
 - in `ssrnum.v`, new lemmas:
   + `(real_)ltr_normlW`, `(real_)ltrNnormlW`, `(real_)ler_normlW`, `(real_)lerNnormlW`
-  + `(real_)ltr_distl_addr`, `(real_)ler_distl_addr`, `(real_)ltr_distl_addrC`, `(real_)ler_distl_addrC`,
-    `(real_)ltr_distl_subl`, `(real_)ler_distl_subl`, `(real_)ltr_distl_sublC`, `(real_)ler_distl_sublC`
+  + `(real_)ltr_distl_addr`, `(real_)ler_distl_addr`, `(real_)ltr_distlC_addr`, `(real_)ler_distlC_addr`,
+    `(real_)ltr_distl_subl`, `(real_)ler_distl_subl`, `(real_)ltr_distlC_subl`, `(real_)ler_distlC_subl`
 
 ### Changed
 
diff --git a/mathcomp/algebra/ssrnum.v b/mathcomp/algebra/ssrnum.v
index 8184577..95c40cd 100644
--- a/mathcomp/algebra/ssrnum.v
+++ b/mathcomp/algebra/ssrnum.v
@@ -2924,10 +2924,10 @@ Proof. by move=> ?; rewrite real_ltr_distl // => /andP[]. Qed.
 Lemma real_ler_distl_addr x y e : x - y \is real -> `|x - y| <= e -> x <= y + e.
 Proof. by move=> ?; rewrite real_ler_distl // => /andP[]. Qed.
 
-Lemma real_ltr_distl_addrC x y e : x - y \is real -> `|x - y| < e -> y < x + e.
+Lemma real_ltr_distlC_addr x y e : x - y \is real -> `|x - y| < e -> y < x + e.
 Proof. by rewrite realBC (distrC x) => ? /real_ltr_distl_addr; apply. Qed.
 
-Lemma real_ler_distl_addrC x y e : x - y \is real -> `|x - y| <= e -> y <= x + e.
+Lemma real_ler_distlC_addr x y e : x - y \is real -> `|x - y| <= e -> y <= x + e.
 Proof. by rewrite realBC distrC => ? /real_ler_distl_addr; apply. Qed.
 
 Lemma real_ltr_distl_subl x y e : x - y \is real -> `|x - y| < e -> x - e < y.
@@ -2936,10 +2936,10 @@ Proof. by move/real_ltr_distl_addr; rewrite ltr_sub_addr; apply. Qed.
 Lemma real_ler_distl_subl x y e : x - y \is real -> `|x - y| <= e -> x - e <= y.
 Proof. by move/real_ler_distl_addr; rewrite ler_sub_addr; apply. Qed.
 
-Lemma real_ltr_distl_sublC x y e : x - y \is real -> `|x - y| < e -> y - e < x.
+Lemma real_ltr_distlC_subl x y e : x - y \is real -> `|x - y| < e -> y - e < x.
 Proof. by rewrite realBC distrC => ? /real_ltr_distl_subl; apply. Qed.
 
-Lemma real_ler_distl_sublC x y e : x - y \is real -> `|x - y| <= e -> y - e <= x.
+Lemma real_ler_distlC_subl x y e : x - y \is real -> `|x - y| <= e -> y - e <= x.
 Proof. by rewrite realBC distrC => ? /real_ler_distl_subl; apply. Qed.
 
 (* GG: pointless duplication }-( *)
@@ -3804,11 +3804,11 @@ Proof. exact: real_ltr_distl_addr. Qed.
 Lemma ler_distl_addr x y e : `|x - y| <= e -> x <= y + e.
 Proof. exact: real_ler_distl_addr. Qed.
 
-Lemma ltr_distl_addrC x y e : `|x - y| < e -> y < x + e.
-Proof. exact: real_ltr_distl_addrC. Qed.
+Lemma ltr_distlC_addr x y e : `|x - y| < e -> y < x + e.
+Proof. exact: real_ltr_distlC_addr. Qed.
 
-Lemma ler_distl_addrC x y e : `|x - y| <= e -> y <= x + e.
-Proof. exact: real_ler_distl_addrC. Qed.
+Lemma ler_distlC_addr x y e : `|x - y| <= e -> y <= x + e.
+Proof. exact: real_ler_distlC_addr. Qed.
 
 Lemma ltr_distl_subl x y e : `|x - y| < e -> x - e < y.
 Proof. exact: real_ltr_distl_subl. Qed.
@@ -3816,11 +3816,11 @@ Proof. exact: real_ltr_distl_subl. Qed.
 Lemma ler_distl_subl x y e : `|x - y| <= e -> x - e <= y.
 Proof. exact: real_ler_distl_subl. Qed.
 
-Lemma ltr_distl_sublC x y e : `|x - y| < e -> y - e < x.
-Proof. exact: real_ltr_distl_sublC. Qed.
+Lemma ltr_distlC_subl x y e : `|x - y| < e -> y - e < x.
+Proof. exact: real_ltr_distlC_subl. Qed.
 
-Lemma ler_distl_subrC x y e : `|x - y| <= e -> y - e <= x.
-Proof. exact: real_ler_distl_sublC. Qed.
+Lemma ler_distlC_subr x y e : `|x - y| <= e -> y - e <= x.
+Proof. exact: real_ler_distlC_subl. Qed.
 
 Lemma exprn_even_ge0 n x : ~~ odd n -> 0 <= x ^+ n.
 Proof. by move=> even_n; rewrite real_exprn_even_ge0 ?num_real. Qed.