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

---
 mathcomp/algebra/ssrnum.v | 6 ++++++
 1 file changed, 6 insertions(+)

(limited to 'mathcomp')

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