From 9bfa00b23ca0306f5f911338bccd625201a4f6d8 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 18 Jun 2018 18:57:50 +0200
Subject: [PATCH] add lemma about chained difference

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

diff --git a/theories/collections.v b/theories/collections.v
index 9ba5d650..e4869e00 100644
--- a/theories/collections.v
+++ b/theories/collections.v
@@ -622,7 +622,8 @@ Section collection.
   Proof. set_solver. Qed.
   Lemma subset_difference_elem_of {x: A} {s: C} (inx: x ∈ s): s ∖ {[ x ]} ⊂ s.
   Proof. set_solver. Qed.
-
+  Lemma difference_difference X Y Z : (X ∖ Y) ∖ Z ≡ X ∖ (Y ∪ Z).
+  Proof. set_solver. Qed.
 
   Lemma difference_mono X1 X2 Y1 Y2 :
     X1 ⊆ X2 → Y2 ⊆ Y1 → X1 ∖ Y1 ⊆ X2 ∖ Y2.
@@ -688,6 +689,8 @@ Section collection.
     Proof. unfold_leibniz. apply difference_intersection_distr_l. Qed.
     Lemma difference_disjoint_L X Y : X ## Y → X ∖ Y = X.
     Proof. unfold_leibniz. apply difference_disjoint. Qed.
+    Lemma difference_difference_L X Y Z : (X ∖ Y) ∖ Z = X ∖ (Y ∪ Z).
+    Proof. unfold_leibniz. apply difference_difference. Qed.
 
     (** Disjointness *)
     Lemma disjoint_intersection_L X Y : X ## Y ↔ X ∩ Y = ∅.
-- 
GitLab