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

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

(limited to 'mathcomp')

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