From d6875e7d4b95f5b1638421c46d4defe80e670b80 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sun, 2 Oct 2016 23:16:05 +0200
Subject: [PATCH] Prove fact about exclusive and included.

---
 algebra/cmra.v | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/algebra/cmra.v b/algebra/cmra.v
index 41e9c0437..93ee00523 100644
--- a/algebra/cmra.v
+++ b/algebra/cmra.v
@@ -344,6 +344,10 @@ Lemma exclusive_r x `{!Exclusive x} y : ✓ (y ⋅ x) → False.
 Proof. rewrite comm. by apply exclusive_l. Qed.
 Lemma exclusiveN_opM n x `{!Exclusive x} my : ✓{n} (x ⋅? my) → my = None.
 Proof. destruct my as [y|]. move=> /(exclusiveN_l _ x) []. done. Qed.
+Lemma exclusive_includedN n x `{!Exclusive x} y : x ≼{n} y → ✓{n} y → False.
+Proof. intros [? ->]. by apply exclusiveN_l. Qed.
+Lemma exclusive_included x `{!Exclusive x} y : x ≼ y → ✓ y → False.
+Proof. intros [? ->]. by apply exclusive_l. Qed.
 
 (** ** Order *)
 Lemma cmra_included_includedN n x y : x ≼ y → x ≼{n} y.
-- 
GitLab