From 6cb0f4d21785d0edbe511be12f730b55fd562331 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 28 Nov 2017 23:36:27 +0100
Subject: [PATCH] Some lemmas about discreteness.

---
 theories/algebra/cmra.v | 4 ++++
 theories/algebra/ofe.v  | 4 +---
 2 files changed, 5 insertions(+), 3 deletions(-)

diff --git a/theories/algebra/cmra.v b/theories/algebra/cmra.v
index 27fc8f8d4..1323605d1 100644
--- a/theories/algebra/cmra.v
+++ b/theories/algebra/cmra.v
@@ -555,11 +555,15 @@ Proof.
   split; first by rewrite cmra_valid_validN.
   eauto using cmra_discrete_valid, cmra_validN_le with lia.
 Qed.
+Lemma cmra_discrete_valid_iff_0 `{CmraDiscrete A} n x : ✓{0} x ↔ ✓{n} x.
+Proof. by rewrite -!cmra_discrete_valid_iff. Qed.
 Lemma cmra_discrete_included_iff `{OfeDiscrete A} n x y : x ≼ y ↔ x ≼{n} y.
 Proof.
   split; first by apply cmra_included_includedN.
   intros [z ->%(discrete_iff _ _)]; eauto using cmra_included_l.
 Qed.
+Lemma cmra_discrete_included_iff_0 `{OfeDiscrete A} n x y : x ≼{0} y ↔ x ≼{n} y.
+Proof. by rewrite -!cmra_discrete_included_iff. Qed.
 
 (** Cancelable elements  *)
 Global Instance cancelable_proper : Proper (equiv ==> iff) (@Cancelable A).
diff --git a/theories/algebra/ofe.v b/theories/algebra/ofe.v
index eb422ac9b..12686722d 100644
--- a/theories/algebra/ofe.v
+++ b/theories/algebra/ofe.v
@@ -190,9 +190,7 @@ Section ofe.
     split; intros; auto. apply (discrete _), dist_le with n; auto with lia.
   Qed.
   Lemma discrete_iff_0 n (x : A) `{!Discrete x} y : x ≡{0}≡ y ↔ x ≡{n}≡ y.
-  Proof.
-    split=> ?. by apply equiv_dist, (discrete _). eauto using dist_le with lia.
-  Qed.
+  Proof. by rewrite -!discrete_iff. Qed.
 End ofe.
 
 (** Contractive functions *)
-- 
GitLab