tentative change of naming convention and add variants

2 files changed, 20 insertions, 5 deletions

diff --git a/mathcomp/algebra/ssralg.v b/mathcomp/algebra/ssralg.v
index 0e71c86..2bde8dd 100644
--- a/mathcomp/algebra/ssralg.v
+++ b/mathcomp/algebra/ssralg.v
@@ -764,9 +764,6 @@ Proof. by rewrite opprD addrA addrK. Qed.
 Lemma subrKA z x y : (x - z) + (z + y) = x + y.
 Proof. by rewrite addrA addrNK. Qed.
 
-Lemma subr_trans z x y : (x - z) + (z - y) = x - y.
-Proof. by rewrite addrA addrNK. Qed.
-
 Lemma addr0_eq x y : x + y = 0 -> - x = y.
 Proof. by rewrite -[-x]addr0 => <-; rewrite addKr. Qed.
 
diff --git a/mathcomp/algebra/ssrnum.v b/mathcomp/algebra/ssrnum.v
index 41199eb..7a41745 100644
--- a/mathcomp/algebra/ssrnum.v
+++ b/mathcomp/algebra/ssrnum.v
@@ -3754,12 +3754,30 @@ Proof. by rewrite lter_norml !lter_sub_addl. Qed.
 
 Definition lter_distl := (ler_distl, ltr_distl).
 
-Lemma ltr_distW x y e : `|x - y| < e -> y - e < x.
+Lemma ltr_dist_addl x y e : `|x - y| < e -> x < y + e.
 Proof. by rewrite ltr_distl => /andP[]. Qed.
 
-Lemma ler_distW x y e : `|x - y| <= e -> y - e <= x.
+Lemma ler_dist_addl x y e : `|x - y| <= e -> x <= y + e.
 Proof. by rewrite ler_distl => /andP[]. Qed.
 
+Lemma ltr_distr_addl x y e : `|x - y| < e -> y < x + e.
+Proof. by rewrite distrC => /ltr_dist_addl. Qed.
+
+Lemma ler_distr_addl x y e : `|x - y| <= e -> y <= x + e.
+Proof. by rewrite distrC => /ler_dist_addl. Qed.
+
+Lemma ltr_dist_subl x y e : `|x - y| < e -> x - e < y.
+Proof. by move/ltr_dist_addl; rewrite -ltr_subl_addr. Qed.
+
+Lemma ler_dist_subl x y e : `|x - y| <= e -> x - e <= y.
+Proof. by move/ler_dist_addl; rewrite -ler_subl_addr. Qed.
+
+Lemma ltr_distr_subr x y e : `|x - y| < e -> y - e < x.
+Proof. by rewrite distrC => /ltr_dist_subl. Qed.
+
+Lemma ler_distr_subr x y e : `|x - y| <= e -> y - e <= x.
+Proof. by rewrite distrC => /ler_dist_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.