From 8e762b5182409053c841ae0287c15ae4a7aa6d9e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Bj=C3=B6rn=20Brandenburg?= <bbb@mpi-sws.org>
Date: Tue, 16 Jul 2019 08:50:51 +0200
Subject: [PATCH] introduce a utility lemma on points outside of intervals

Points before or after an interval are not in the interval...
---
 util/nat.v | 20 ++++++++++++++++++++
 1 file changed, 20 insertions(+)

diff --git a/util/nat.v b/util/nat.v
index 61c64e7..59f5a64 100644
--- a/util/nat.v
+++ b/util/nat.v
@@ -120,6 +120,26 @@ Section NatLemmas.
 
 End NatLemmas.
 
+Section Interval.
+
+  (* Trivially, points before the start of an interval, or past the end of an
+     interval, are not included in the interval. *)
+  Lemma point_not_in_interval:
+    forall t1 t2 t',
+      t2 <= t' \/ t' < t1 ->
+      forall t,
+        t1 <= t < t2
+        -> t <> t'.
+  Proof.
+    move=> t1 t2 t' EXCLUDED t /andP [GEQ_t1 LT_t2] EQ.
+    subst.
+    case EXCLUDED => [INEQ | INEQ];
+      eapply leq_ltn_trans in INEQ; eauto;
+      by rewrite ltnn in INEQ.
+  Qed.
+
+End Interval.
+
 Section NatOrderLemmas.
 
   (* Mimic the way implicit arguments are used in ssreflect. *)
-- 
GitLab