From 425c0d18a952e6312a1df392f02010d6c5f72982 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 21 Feb 2019 12:19:25 +0100
Subject: [PATCH] =?UTF-8?q?Lemma=20for=20`x=20=E2=88=88=20=5F=20=E2=8A=8E?=
 =?UTF-8?q?=20=5F`=20on=20multisets.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 theories/gmultiset.v | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

diff --git a/theories/gmultiset.v b/theories/gmultiset.v
index 9ca8a767..be9c4911 100644
--- a/theories/gmultiset.v
+++ b/theories/gmultiset.v
@@ -126,12 +126,14 @@ Qed.
 Global Instance gmultiset_elem_of_dec : RelDecision (∈@{gmultiset A}).
 Proof. refine (λ x X, cast_if (decide (0 < multiplicity x X))); done. Defined.
 
+Lemma gmultiset_elem_of_disj_union X Y x : x ∈ X ⊎ Y ↔ x ∈ X ∨ x ∈ Y.
+Proof. rewrite !elem_of_multiplicity, multiplicity_disj_union. lia. Qed.
+
 Global Instance set_unfold_gmultiset_disj_union x X Y P Q :
   SetUnfold (x ∈ X) P → SetUnfold (x ∈ Y) Q → SetUnfold (x ∈ X ⊎ Y) (P ∨ Q).
 Proof.
-  intros ??; constructor.
-  rewrite <-(set_unfold (x ∈ X) P), <-(set_unfold (x ∈ Y) Q).
-  rewrite !elem_of_multiplicity, multiplicity_disj_union. lia.
+  intros ??; constructor. rewrite gmultiset_elem_of_disj_union.
+  by rewrite <-(set_unfold (x ∈ X) P), <-(set_unfold (x ∈ Y) Q).
 Qed.
 
 (* Algebraic laws *)
-- 
GitLab