From a70caa4bc04caf1bd23cd4c4e450501f5bd06fd0 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 9 May 2018 23:28:03 +0200
Subject: [PATCH] All multiset elements are cancelable.

---
 theories/algebra/gmultiset.v | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/theories/algebra/gmultiset.v b/theories/algebra/gmultiset.v
index 86a1fc0c8..c3bcfa600 100644
--- a/theories/algebra/gmultiset.v
+++ b/theories/algebra/gmultiset.v
@@ -50,6 +50,11 @@ Section gmultiset.
   Proof. split. done. intros X. by rewrite gmultiset_op_union left_id_L. done. Qed.
   Canonical Structure gmultisetUR := UcmraT (gmultiset K) gmultiset_ucmra_mixin.
 
+  Global Instance gmultiset_cancelable X : Cancelable X.
+  Proof.
+    apply: discrete_cancelable=> Y Z _ ?. fold_leibniz. by apply (inj (X ∪)).
+  Qed.
+
   Lemma gmultiset_opM X mY : X ⋅? mY = X ∪ from_option id ∅ mY.
   Proof. destruct mY; by rewrite /= ?right_id_L. Qed.
 
@@ -71,7 +76,6 @@ Section gmultiset.
     repeat (rewrite multiplicity_difference || rewrite multiplicity_union).
     omega.
   Qed.
-
 End gmultiset.
 
 Arguments gmultisetC _ {_ _}.
-- 
GitLab