From 81d719c9414454cfd2c1505ccb6b6fe92ffbd80f Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 9 Mar 2017 23:07:17 +0100
Subject: [PATCH] =?UTF-8?q?Mononicity=20of=20=E2=88=96.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 theories/collections.v | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

diff --git a/theories/collections.v b/theories/collections.v
index a37e1365..28a8f25b 100644
--- a/theories/collections.v
+++ b/theories/collections.v
@@ -346,7 +346,6 @@ Section simple_collection.
   Proof. set_solver. Qed.
   Lemma elem_of_union_r x X Y : x ∈ Y → x ∈ X ∪ Y.
   Proof. set_solver. Qed.
-
   Lemma union_preserving_l X Y1 Y2 : Y1 ⊆ Y2 → X ∪ Y1 ⊆ X ∪ Y2.
   Proof. set_solver. Qed.
   Lemma union_preserving_r X1 X2 Y : X1 ⊆ X2 → X1 ∪ Y ⊆ X2 ∪ Y.
@@ -613,6 +612,14 @@ Section collection.
   Lemma difference_disjoint X Y : X ⊥ Y → X ∖ Y ≡ X.
   Proof. set_solver. Qed.
 
+  Lemma difference_preserving X1 X2 Y1 Y2 :
+    X1 ⊆ X2 → Y2 ⊆ Y1 → X1 ∖ Y1 ⊆ X2 ∖ Y2.
+  Proof. set_solver. Qed.
+  Lemma difference_preserving_l X Y1 Y2 : Y2 ⊆ Y1 → X ∖ Y1 ⊆ X ∖ Y2.
+  Proof. set_solver. Qed.
+  Lemma difference_preserving_r X1 X2 Y : X1 ⊆ X2 → X1 ∖ Y ⊆ X2 ∖ Y.
+  Proof. set_solver. Qed.
+
   (** Disjointness *)
   Lemma disjoint_intersection X Y : X ⊥ Y ↔ X ∩ Y ≡ ∅.
   Proof. set_solver. Qed.
-- 
GitLab