From e0ea56587f7ae43eb413e3e20956e01e4c66ff62 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 9 Sep 2021 17:22:43 -0400
Subject: [PATCH] add size_difference

---
 theories/fin_sets.v | 11 +++++++++++
 1 file changed, 11 insertions(+)

diff --git a/theories/fin_sets.v b/theories/fin_sets.v
index 14aef32f..2e72335f 100644
--- a/theories/fin_sets.v
+++ b/theories/fin_sets.v
@@ -193,6 +193,17 @@ Proof.
   rewrite <-union_difference, (comm (∪)); set_solver.
 Qed.
 
+Lemma size_difference X Y : Y ⊆ X → size (X ∖ Y) = size X - size Y.
+Proof.
+  intros. rewrite (union_difference Y X) at 2 by done.
+  rewrite size_union by set_solver. lia.
+Qed.
+Lemma size_difference_alt X Y : size (X ∖ Y) = size X - size (X ∩ Y).
+Proof.
+  intros. rewrite <-size_difference by set_solver.
+  apply set_size_proper. set_solver.
+Qed.
+
 Lemma subseteq_size X Y : X ⊆ Y → size X ≤ size Y.
 Proof. intros. rewrite (union_difference X Y), size_union_alt by done. lia. Qed.
 Lemma subset_size X Y : X ⊂ Y → size X < size Y.
-- 
GitLab