From 652aebfce4b5a76e193493cac7482cf5d65ead59 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 22 Feb 2017 19:02:59 +0100
Subject: [PATCH] show that dist_later is a subrelation of dist

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

diff --git a/theories/algebra/ofe.v b/theories/algebra/ofe.v
index eeefadec8..7a722900b 100644
--- a/theories/algebra/ofe.v
+++ b/theories/algebra/ofe.v
@@ -189,6 +189,9 @@ Arguments dist_later _ !_ _ _ /.
 Global Instance dist_later_equivalence A n : Equivalence (@dist_later A n).
 Proof. destruct n as [|n]. by split. apply dist_equivalence. Qed.
 
+Lemma dist_dist_later {A : ofeT} n (x y : A) : dist n x y → dist_later n x y.
+Proof. intros Heq. destruct n; first done. exact: dist_S. Qed.
+
 Notation Contractive f := (∀ n, Proper (dist_later n ==> dist n) f).
 
 Instance const_contractive {A B : ofeT} (x : A) : Contractive (@const A B x).
-- 
GitLab