From b73112e3bf98965dd9db58a69d2f5c0d83203ee9 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 13 Apr 2017 17:27:16 +0200
Subject: [PATCH] Lemma timeless_iff_0.

---
 theories/algebra/ofe.v | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/theories/algebra/ofe.v b/theories/algebra/ofe.v
index 9bb911c34..bd5f3e386 100644
--- a/theories/algebra/ofe.v
+++ b/theories/algebra/ofe.v
@@ -183,10 +183,15 @@ Section ofe.
     transitivity (c n); first by apply conv_compl. symmetry.
     apply chain_cauchy. omega.
   Qed.
+
   Lemma timeless_iff n (x : A) `{!Timeless x} y : x ≡ y ↔ x ≡{n}≡ y.
   Proof.
     split; intros; auto. apply (timeless _), dist_le with n; auto with lia.
   Qed.
+  Lemma timeless_iff_0 n (x : A) `{!Timeless x} y : x ≡{0}≡ y ↔ x ≡{n}≡ y.
+  Proof.
+    split=> ?. by apply equiv_dist, (timeless _). eauto using dist_le with lia.
+  Qed.
 End ofe.
 
 (** Contractive functions *)
-- 
GitLab