From 83e8892161c8ef3903e302c82a2a7a43f2708d67 Mon Sep 17 00:00:00 2001
From: Reynald Affeldt
Date: Thu, 21 May 2020 23:32:46 +0900
Subject: three lemmas that we found useful in the context of the
 mathcomp-analysis project

---
 CHANGELOG_UNRELEASED.md   | 2 ++
 mathcomp/algebra/ssralg.v | 3 +++
 mathcomp/algebra/ssrnum.v | 6 ++++++
 3 files changed, 11 insertions(+)

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 13e1d1b..53ee464 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -10,6 +10,8 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/).
 
 ### Added
 
+- lemma `subr_trans` in `ssralg` and lemmas `ltr_distW` and `ler_distW` in `ssrnum`
+
 ### Changed
 
 ### Renamed
diff --git a/mathcomp/algebra/ssralg.v b/mathcomp/algebra/ssralg.v
index 2bde8dd..0e71c86 100644
--- a/mathcomp/algebra/ssralg.v
+++ b/mathcomp/algebra/ssralg.v
@@ -764,6 +764,9 @@ 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 e1e5992..41199eb 100644
--- a/mathcomp/algebra/ssrnum.v
+++ b/mathcomp/algebra/ssrnum.v
@@ -3754,6 +3754,12 @@ 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.
+Proof. by rewrite ltr_distl => /andP[]. Qed.
+
+Lemma ler_distW x y e : `|x - y| <= e -> y - e <= x.
+Proof. by rewrite ler_distl => /andP[]. 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.
 
-- 
cgit v1.2.3


From a65958322cb6ee84f3ebbb68d1fb4867749cf1a0 Mon Sep 17 00:00:00 2001
From: Reynald Affeldt
Date: Fri, 22 May 2020 03:52:40 +0900
Subject: tentative change of naming convention and add variants

---
 CHANGELOG_UNRELEASED.md   |  4 +++-
 mathcomp/algebra/ssralg.v |  3 ---
 mathcomp/algebra/ssrnum.v | 22 ++++++++++++++++++++--
 3 files changed, 23 insertions(+), 6 deletions(-)

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 53ee464..957e02c 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -10,7 +10,9 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/).
 
 ### Added
 
-- lemma `subr_trans` in `ssralg` and lemmas `ltr_distW` and `ler_distW` in `ssrnum`
+- lemmas `ltr_dist_addl`, `ler_dist_addl`, `ltr_distr_addl`,
+  `ler_distr_addl`, `ltr_dist_subl`, `ler_dist_subl`,
+  `ltr_distr_subr`, `ler_distr_subr` in `ssrnum`
 
 ### Changed
 
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.
 
-- 
cgit v1.2.3


From 3d77e498c075af6f642b3239acf4b18503c1e6bc Mon Sep 17 00:00:00 2001
From: Reynald Affeldt
Date: Tue, 2 Jun 2020 18:14:22 +0900
Subject: another lemma about norm from mathcomp-analysis

---
 CHANGELOG_UNRELEASED.md   | 2 +-
 mathcomp/algebra/ssrnum.v | 6 ++++++
 2 files changed, 7 insertions(+), 1 deletion(-)

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 957e02c..4de3f44 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -12,7 +12,7 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/).
 
 - lemmas `ltr_dist_addl`, `ler_dist_addl`, `ltr_distr_addl`,
   `ler_distr_addl`, `ltr_dist_subl`, `ler_dist_subl`,
-  `ltr_distr_subr`, `ler_distr_subr` in `ssrnum`
+  `ltr_distr_subr`, `ler_distr_subr`, `norm_lt_eqF` in `ssrnum`
 
 ### Changed
 
diff --git a/mathcomp/algebra/ssrnum.v b/mathcomp/algebra/ssrnum.v
index 7a41745..5047868 100644
--- a/mathcomp/algebra/ssrnum.v
+++ b/mathcomp/algebra/ssrnum.v
@@ -3778,6 +3778,12 @@ 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 norm_lt_eqF (x y : R) : `|x| < y -> (x == - y = false) * (x == y = false).
+Proof.
+move=> x1; split; last by rewrite lt_eqF // (le_lt_trans (ler_norm _) x1).
+by move: x1; rewrite ltr_norml => /andP[? ?]; rewrite gt_eqF.
+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.
 
-- 
cgit v1.2.3


From e5165bd0bb3ba31c7ecc95f99e1c43353feca987 Mon Sep 17 00:00:00 2001
From: Reynald Affeldt
Date: Wed, 3 Jun 2020 04:48:09 +0900
Subject: add real_* variants

---
 CHANGELOG_UNRELEASED.md   |  8 +++---
 mathcomp/algebra/ssrnum.v | 64 +++++++++++++++++++++++++++++++++++++++--------
 2 files changed, 59 insertions(+), 13 deletions(-)

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 4de3f44..6e86ad6 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -10,9 +10,11 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/).
 
 ### Added
 
-- lemmas `ltr_dist_addl`, `ler_dist_addl`, `ltr_distr_addl`,
-  `ler_distr_addl`, `ltr_dist_subl`, `ler_dist_subl`,
-  `ltr_distr_subr`, `ler_distr_subr`, `norm_lt_eqF` in `ssrnum`
+- in `ssrnum.v`, new lemmas:
+  + `gt_norm_eqF`
+  + `{real_,}gtr_norm`, `{real_,}gtrNnorm`, `{real_,}ger_norm`, `{real_,}gerNnorm`
+  + `{real_,}ltr_dist_addl`, `{real_,}ler_dist_addl`, `{real_,}ltr_distr_addl`, `{real_,}ler_distr_addl`,
+    `{real_,}ltr_dist_subl`, `{real_,}ler_dist_subl`, `{real_,}ltr_distr_subr`, `{real_,}ler_distr_subr`
 
 ### Changed
 
diff --git a/mathcomp/algebra/ssrnum.v b/mathcomp/algebra/ssrnum.v
index 5047868..361394a 100644
--- a/mathcomp/algebra/ssrnum.v
+++ b/mathcomp/algebra/ssrnum.v
@@ -2894,7 +2894,19 @@ rewrite real_ltNge ?real_ler_norml // negb_and -?real_ltNge ?realN //.
 by rewrite orbC ltr_oppr.
 Qed.
 
-Definition real_lter_normr :=  (real_ler_normr, real_ltr_normr).
+Definition real_lter_normr := (real_ler_normr, real_ltr_normr).
+
+Lemma real_gtr_norm x y : x \is real -> `|x| < y -> x < y.
+Proof. by move=> ?; case/real_ltr_normlP. Qed.
+
+Lemma real_gtrNnorm x y : x \is real -> `|x| < y -> - y < x.
+Proof. by move=> ?; case/real_ltr_normlP => //; rewrite ltr_oppl. Qed.
+
+Lemma real_ger_norm x y : x \is real -> `|x| <= y -> x <= y.
+Proof. by move=> ?; case/real_ler_normlP. Qed.
+
+Lemma real_gerNnorm x y : x \is real -> `|x| <= y -> - y <= x.
+Proof. by move=> ?; case/real_ler_normlP => //; rewrite ler_oppl. Qed.
 
 Lemma real_ler_distl x y e :
   x - y \is real -> (`|x - y| <= e) = (y - e <= x <= y + e).
@@ -2906,6 +2918,30 @@ Proof. by move=> Rxy; rewrite real_lter_norml // !lter_sub_addl. Qed.
 
 Definition real_lter_distl := (real_ler_distl, real_ltr_distl).
 
+Lemma real_ltr_dist_addl x y e : x - y \is real -> `|x - y| < e -> x < y + e.
+Proof. by move=> ?; rewrite real_ltr_distl // => /andP[]. Qed.
+
+Lemma real_ler_dist_addl 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_distr_addl x y e : x - y \is real -> `|x - y| < e -> y < x + e.
+Proof. by rewrite realBC (distrC x) => ? /real_ltr_dist_addl; apply. Qed.
+
+Lemma real_ler_distr_addl x y e : x - y \is real -> `|x - y| <= e -> y <= x + e.
+Proof. by rewrite realBC distrC => ? /real_ler_dist_addl; apply. Qed.
+
+Lemma real_ltr_dist_subl x y e : x - y \is real -> `|x - y| < e -> x - e < y.
+Proof. by move/real_ltr_dist_addl; rewrite ltr_sub_addr; apply. Qed.
+
+Lemma real_ler_dist_subl x y e : x - y \is real -> `|x - y| <= e -> x - e <= y.
+Proof. by move/real_ler_dist_addl; rewrite ler_sub_addr; apply. Qed.
+
+Lemma real_ltr_distr_subr x y e : x - y \is real -> `|x - y| < e -> y - e < x.
+Proof. by rewrite realBC distrC => ? /real_ltr_dist_subl; apply. Qed.
+
+Lemma real_ler_distr_subr x y e : x - y \is real -> `|x - y| <= e -> y - e <= x.
+Proof. by rewrite realBC distrC => ? /real_ler_dist_subl; apply. Qed.
+
 (* GG: pointless duplication }-( *)
 Lemma eqr_norm_id x : (`|x| == x) = (0 <= x). Proof. by rewrite ger0_def. Qed.
 Lemma eqr_normN x : (`|x| == - x) = (x <= 0). Proof. by rewrite ler0_def. Qed.
@@ -3738,6 +3774,14 @@ Lemma ltr_normlP x y : reflect ((-x < y) * (x < y)) (`|x| < y).
 Proof. exact: real_ltr_normlP. Qed.
 Arguments ltr_normlP {x y}.
 
+Lemma gtr_norm x y : `|x| < y -> x < y. Proof. exact: real_gtr_norm. Qed.
+
+Lemma gtrNnorm x y : `|x| < y -> - y < x. Proof. exact: real_gtrNnorm. Qed.
+
+Lemma ger_norm x y : `|x| <= y -> x <= y. Proof. exact: real_ger_norm. Qed.
+
+Lemma gerNnorm x y : `|x| <= y -> - y <= x. Proof. exact: real_gerNnorm. Qed.
+
 Lemma ler_normr x y : (x <= `|y|) = (x <= y) || (x <= - y).
 Proof. by rewrite leNgt ltr_norml negb_and -!leNgt orbC ler_oppr. Qed.
 
@@ -3755,30 +3799,30 @@ Proof. by rewrite lter_norml !lter_sub_addl. Qed.
 Definition lter_distl := (ler_distl, ltr_distl).
 
 Lemma ltr_dist_addl x y e : `|x - y| < e -> x < y + e.
-Proof. by rewrite ltr_distl => /andP[]. Qed.
+Proof. exact: real_ltr_dist_addl. Qed.
 
 Lemma ler_dist_addl x y e : `|x - y| <= e -> x <= y + e.
-Proof. by rewrite ler_distl => /andP[]. Qed.
+Proof. exact: real_ler_dist_addl. Qed.
 
 Lemma ltr_distr_addl x y e : `|x - y| < e -> y < x + e.
-Proof. by rewrite distrC => /ltr_dist_addl. Qed.
+Proof. exact: real_ltr_distr_addl. Qed.
 
 Lemma ler_distr_addl x y e : `|x - y| <= e -> y <= x + e.
-Proof. by rewrite distrC => /ler_dist_addl. Qed.
+Proof. exact: real_ler_distr_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.
+Proof. exact: real_ltr_dist_subl. 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.
+Proof. exact: real_ler_dist_subl. Qed.
 
 Lemma ltr_distr_subr x y e : `|x - y| < e -> y - e < x.
-Proof. by rewrite distrC => /ltr_dist_subl. Qed.
+Proof. exact: real_ltr_distr_subr. Qed.
 
 Lemma ler_distr_subr x y e : `|x - y| <= e -> y - e <= x.
-Proof. by rewrite distrC => /ler_dist_subl. Qed.
+Proof. exact: real_ler_distr_subr. Qed.
 
-Lemma norm_lt_eqF (x y : R) : `|x| < y -> (x == - y = false) * (x == y = false).
+Lemma gt_norm_eqF (x y : R) : `|x| < y -> (x == - y = false) * (x == y = false).
 Proof.
 move=> x1; split; last by rewrite lt_eqF // (le_lt_trans (ler_norm _) x1).
 by move: x1; rewrite ltr_norml => /andP[? ?]; rewrite gt_eqF.
-- 
cgit v1.2.3


From 0a999b90fb9517849b70a8bb28895b0e905af2b4 Mon Sep 17 00:00:00 2001
From: Reynald Affeldt
Date: Thu, 4 Jun 2020 19:25:53 +0900
Subject: fix naming

---
 CHANGELOG_UNRELEASED.md   |  7 ++--
 CONTRIBUTING.md           | 10 ++++--
 mathcomp/algebra/ssrnum.v | 90 ++++++++++++++++++++++-------------------------
 3 files changed, 52 insertions(+), 55 deletions(-)

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 6e86ad6..6f98d3c 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -11,10 +11,9 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/).
 ### Added
 
 - in `ssrnum.v`, new lemmas:
-  + `gt_norm_eqF`
-  + `{real_,}gtr_norm`, `{real_,}gtrNnorm`, `{real_,}ger_norm`, `{real_,}gerNnorm`
-  + `{real_,}ltr_dist_addl`, `{real_,}ler_dist_addl`, `{real_,}ltr_distr_addl`, `{real_,}ler_distr_addl`,
-    `{real_,}ltr_dist_subl`, `{real_,}ler_dist_subl`, `{real_,}ltr_distr_subr`, `{real_,}ler_distr_subr`
+  + `{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`
 
 ### Changed
 
diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md
index 6313d01..ea5d631 100644
--- a/CONTRIBUTING.md
+++ b/CONTRIBUTING.md
@@ -124,7 +124,9 @@ Abbreviations are in the header of the file which introduces them. We list here
   - `g` -- a group argument.
   - `I` -- left/right injectivity, as in `addbI : right_injective addb.`
         -- alternatively predicate or set intersection, as in `predI.`
-  - `l` -- the left-hand of an operation, as in `andb_orl : left_distributive andb orb.`
+  - `l` -- the left-hand of an operation, as in
+    + `andb_orl : left_distributive andb orb.`
+    + `ltr_norml x y : (`|x| < y) = (- y < x < y).`
   - `L` -- the left-hand of a relation, as in `ltn_subrL : n - m < n = (0 < m) && (0 < n).`
   - `LR` -- moving an operator from the left-hand to the right-hand of an relation, as in `leq_subLR : (m - n <= p) = (m <= n + p).`
   - `N` or `n` -- boolean negation, as in `andbN : a && (~~ a) = false.`
@@ -132,8 +134,10 @@ Abbreviations are in the header of the file which introduces them. We list here
   - `N` -- alternatively ring negation, as in `mulNr : (- x) * y = - (x * y).`
   - `P` -- a characteristic property, often a reflection lemma, as in
      `andP : reflect (a /\ b) (a && b)`.
-  - `r` -- a right-hand operation, as `orb_andr : right_distributive orb andb.`
-      -- alternatively, it is a ring argument.
+  - `r` -- a right-hand operation, as in
+    + `orb_andr : right_distributive orb andb.`
+    + `ler_normr x y : (x <= `|y|) = (x <= y) || (x <= - y).`
+    + alternatively, it is a ring argument.
   - `R` -- the right-hand of a relation, as in `ltn_subrR : n < n - m = false`.
   - `RL` -- moving an operator from the right-hand to the left-hand of an relation, as in `ltn_subRL : (n < p - m) = (m + n < p).`
   - `T` or `t` -- boolean truth, as in `andbT: right_id true andb.`
diff --git a/mathcomp/algebra/ssrnum.v b/mathcomp/algebra/ssrnum.v
index 361394a..8184577 100644
--- a/mathcomp/algebra/ssrnum.v
+++ b/mathcomp/algebra/ssrnum.v
@@ -2896,16 +2896,16 @@ Qed.
 
 Definition real_lter_normr := (real_ler_normr, real_ltr_normr).
 
-Lemma real_gtr_norm x y : x \is real -> `|x| < y -> x < y.
+Lemma real_ltr_normlW x y : x \is real -> `|x| < y -> x < y.
 Proof. by move=> ?; case/real_ltr_normlP. Qed.
 
-Lemma real_gtrNnorm x y : x \is real -> `|x| < y -> - y < x.
+Lemma real_ltrNnormlW x y : x \is real -> `|x| < y -> - y < x.
 Proof. by move=> ?; case/real_ltr_normlP => //; rewrite ltr_oppl. Qed.
 
-Lemma real_ger_norm x y : x \is real -> `|x| <= y -> x <= y.
+Lemma real_ler_normlW x y : x \is real -> `|x| <= y -> x <= y.
 Proof. by move=> ?; case/real_ler_normlP. Qed.
 
-Lemma real_gerNnorm x y : x \is real -> `|x| <= y -> - y <= x.
+Lemma real_lerNnormlW x y : x \is real -> `|x| <= y -> - y <= x.
 Proof. by move=> ?; case/real_ler_normlP => //; rewrite ler_oppl. Qed.
 
 Lemma real_ler_distl x y e :
@@ -2918,29 +2918,29 @@ Proof. by move=> Rxy; rewrite real_lter_norml // !lter_sub_addl. Qed.
 
 Definition real_lter_distl := (real_ler_distl, real_ltr_distl).
 
-Lemma real_ltr_dist_addl x y e : x - y \is real -> `|x - y| < e -> x < y + e.
+Lemma real_ltr_distl_addr x y e : x - y \is real -> `|x - y| < e -> x < y + e.
 Proof. by move=> ?; rewrite real_ltr_distl // => /andP[]. Qed.
 
-Lemma real_ler_dist_addl x y e : x - y \is real -> `|x - y| <= e -> x <= y + e.
+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_distr_addl x y e : x - y \is real -> `|x - y| < e -> y < x + e.
-Proof. by rewrite realBC (distrC x) => ? /real_ltr_dist_addl; apply. Qed.
+Lemma real_ltr_distl_addrC 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_distr_addl x y e : x - y \is real -> `|x - y| <= e -> y <= x + e.
-Proof. by rewrite realBC distrC => ? /real_ler_dist_addl; apply. Qed.
+Lemma real_ler_distl_addrC 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_dist_subl x y e : x - y \is real -> `|x - y| < e -> x - e < y.
-Proof. by move/real_ltr_dist_addl; rewrite ltr_sub_addr; apply. Qed.
+Lemma real_ltr_distl_subl x y e : x - y \is real -> `|x - y| < e -> x - e < y.
+Proof. by move/real_ltr_distl_addr; rewrite ltr_sub_addr; apply. Qed.
 
-Lemma real_ler_dist_subl x y e : x - y \is real -> `|x - y| <= e -> x - e <= y.
-Proof. by move/real_ler_dist_addl; rewrite ler_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_distr_subr x y e : x - y \is real -> `|x - y| < e -> y - e < x.
-Proof. by rewrite realBC distrC => ? /real_ltr_dist_subl; apply. Qed.
+Lemma real_ltr_distl_sublC 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_distr_subr x y e : x - y \is real -> `|x - y| <= e -> y - e <= x.
-Proof. by rewrite realBC distrC => ? /real_ler_dist_subl; apply. Qed.
+Lemma real_ler_distl_sublC 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 }-( *)
 Lemma eqr_norm_id x : (`|x| == x) = (0 <= x). Proof. by rewrite ger0_def. Qed.
@@ -3774,59 +3774,53 @@ Lemma ltr_normlP x y : reflect ((-x < y) * (x < y)) (`|x| < y).
 Proof. exact: real_ltr_normlP. Qed.
 Arguments ltr_normlP {x y}.
 
-Lemma gtr_norm x y : `|x| < y -> x < y. Proof. exact: real_gtr_norm. Qed.
+Lemma ltr_normlW x y : `|x| < y -> x < y. Proof. exact: real_ltr_normlW. Qed.
 
-Lemma gtrNnorm x y : `|x| < y -> - y < x. Proof. exact: real_gtrNnorm. Qed.
+Lemma ltrNnormlW x y : `|x| < y -> - y < x. Proof. exact: real_ltrNnormlW. Qed.
 
-Lemma ger_norm x y : `|x| <= y -> x <= y. Proof. exact: real_ger_norm. Qed.
+Lemma ler_normlW x y : `|x| <= y -> x <= y. Proof. exact: real_ler_normlW. Qed.
 
-Lemma gerNnorm x y : `|x| <= y -> - y <= x. Proof. exact: real_gerNnorm. Qed.
+Lemma lerNnormlW x y : `|x| <= y -> - y <= x. Proof. exact: real_lerNnormlW. Qed.
 
 Lemma ler_normr x y : (x <= `|y|) = (x <= y) || (x <= - y).
-Proof. by rewrite leNgt ltr_norml negb_and -!leNgt orbC ler_oppr. Qed.
+Proof. exact: real_ler_normr. Qed.
 
 Lemma ltr_normr x y : (x < `|y|) = (x < y) || (x < - y).
-Proof. by rewrite ltNge ler_norml negb_and -!ltNge orbC ltr_oppr. Qed.
+Proof. exact: real_ltr_normr. Qed.
 
 Definition lter_normr := (ler_normr, ltr_normr).
 
 Lemma ler_distl x y e : (`|x - y| <= e) = (y - e <= x <= y + e).
-Proof. by rewrite lter_norml !lter_sub_addl. Qed.
+Proof. exact: real_ler_distl. Qed.
 
 Lemma ltr_distl x y e : (`|x - y| < e) = (y - e < x < y + e).
-Proof. by rewrite lter_norml !lter_sub_addl. Qed.
+Proof. exact: real_ltr_distl. Qed.
 
 Definition lter_distl := (ler_distl, ltr_distl).
 
-Lemma ltr_dist_addl x y e : `|x - y| < e -> x < y + e.
-Proof. exact: real_ltr_dist_addl. Qed.
+Lemma ltr_distl_addr x y e : `|x - y| < e -> x < y + e.
+Proof. exact: real_ltr_distl_addr. Qed.
 
-Lemma ler_dist_addl x y e : `|x - y| <= e -> x <= y + e.
-Proof. exact: real_ler_dist_addl. Qed.
+Lemma ler_distl_addr x y e : `|x - y| <= e -> x <= y + e.
+Proof. exact: real_ler_distl_addr. Qed.
 
-Lemma ltr_distr_addl x y e : `|x - y| < e -> y < x + e.
-Proof. exact: real_ltr_distr_addl. Qed.
+Lemma ltr_distl_addrC x y e : `|x - y| < e -> y < x + e.
+Proof. exact: real_ltr_distl_addrC. Qed.
 
-Lemma ler_distr_addl x y e : `|x - y| <= e -> y <= x + e.
-Proof. exact: real_ler_distr_addl. Qed.
+Lemma ler_distl_addrC x y e : `|x - y| <= e -> y <= x + e.
+Proof. exact: real_ler_distl_addrC. Qed.
 
-Lemma ltr_dist_subl x y e : `|x - y| < e -> x - e < y.
-Proof. exact: real_ltr_dist_subl. Qed.
+Lemma ltr_distl_subl x y e : `|x - y| < e -> x - e < y.
+Proof. exact: real_ltr_distl_subl. Qed.
 
-Lemma ler_dist_subl x y e : `|x - y| <= e -> x - e <= y.
-Proof. exact: real_ler_dist_subl. Qed.
+Lemma ler_distl_subl x y e : `|x - y| <= e -> x - e <= y.
+Proof. exact: real_ler_distl_subl. Qed.
 
-Lemma ltr_distr_subr x y e : `|x - y| < e -> y - e < x.
-Proof. exact: real_ltr_distr_subr. Qed.
+Lemma ltr_distl_sublC x y e : `|x - y| < e -> y - e < x.
+Proof. exact: real_ltr_distl_sublC. Qed.
 
-Lemma ler_distr_subr x y e : `|x - y| <= e -> y - e <= x.
-Proof. exact: real_ler_distr_subr. Qed.
-
-Lemma gt_norm_eqF (x y : R) : `|x| < y -> (x == - y = false) * (x == y = false).
-Proof.
-move=> x1; split; last by rewrite lt_eqF // (le_lt_trans (ler_norm _) x1).
-by move: x1; rewrite ltr_norml => /andP[? ?]; rewrite gt_eqF.
-Qed.
+Lemma ler_distl_subrC x y e : `|x - y| <= e -> y - e <= x.
+Proof. exact: real_ler_distl_sublC. 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.
-- 
cgit v1.2.3


From 86c72a2a0164b8af1a95eb3799a8055cfa8fbe2a Mon Sep 17 00:00:00 2001
From: Reynald Affeldt
Date: Thu, 4 Jun 2020 19:28:19 +0900
Subject: fix md formatting

---
 CONTRIBUTING.md | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md
index ea5d631..19ab0e5 100644
--- a/CONTRIBUTING.md
+++ b/CONTRIBUTING.md
@@ -126,7 +126,7 @@ Abbreviations are in the header of the file which introduces them. We list here
         -- alternatively predicate or set intersection, as in `predI.`
   - `l` -- the left-hand of an operation, as in
     + `andb_orl : left_distributive andb orb.`
-    + `ltr_norml x y : (`|x| < y) = (- y < x < y).`
+    + ``ltr_norml x y : (`|x| < y) = (- y < x < y).``
   - `L` -- the left-hand of a relation, as in `ltn_subrL : n - m < n = (0 < m) && (0 < n).`
   - `LR` -- moving an operator from the left-hand to the right-hand of an relation, as in `leq_subLR : (m - n <= p) = (m <= n + p).`
   - `N` or `n` -- boolean negation, as in `andbN : a && (~~ a) = false.`
@@ -136,7 +136,7 @@ Abbreviations are in the header of the file which introduces them. We list here
      `andP : reflect (a /\ b) (a && b)`.
   - `r` -- a right-hand operation, as in
     + `orb_andr : right_distributive orb andb.`
-    + `ler_normr x y : (x <= `|y|) = (x <= y) || (x <= - y).`
+    + ``ler_normr x y : (x <= `|y|) = (x <= y) || (x <= - y).``
     + alternatively, it is a ring argument.
   - `R` -- the right-hand of a relation, as in `ltn_subrR : n < n - m = false`.
   - `RL` -- moving an operator from the right-hand to the left-hand of an relation, as in `ltn_subRL : (n < p - m) = (m + n < p).`
-- 
cgit v1.2.3


From 33c29d4653ac5be781823ae5ede47c361f13d80f Mon Sep 17 00:00:00 2001
From: Reynald Affeldt
Date: Thu, 4 Jun 2020 20:45:53 +0900
Subject: fix changelog

---
 CHANGELOG_UNRELEASED.md | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 6f98d3c..a5fae21 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -11,9 +11,9 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/).
 ### Added
 
 - 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_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`
 
 ### Changed
 
-- 
cgit v1.2.3


From 847cc0eab00c004b52195f8d63a763725524fe2f Mon Sep 17 00:00:00 2001
From: Reynald Affeldt
Date: Fri, 5 Jun 2020 00:49:15 +0900
Subject: fix naming

---
 CHANGELOG_UNRELEASED.md   |  4 ++--
 mathcomp/algebra/ssrnum.v | 24 ++++++++++++------------
 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.
-- 
cgit v1.2.3