From 95cee4756b0a2009f393debcfc6405d3cf0470ce Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 18 Nov 2016 00:27:21 +0100
Subject: [PATCH] More big_opMS lemmas.

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

diff --git a/theories/gmultiset.v b/theories/gmultiset.v
index 51b1a98..0fab06b 100644
--- a/theories/gmultiset.v
+++ b/theories/gmultiset.v
@@ -157,6 +157,14 @@ Proof.
   rewrite multiplicity_difference, multiplicity_empty; omega.
 Qed.
 
+(* Order stuff *)
+Lemma gmultiset_elem_of_subseteq x X : x ∈ X → {[ x ]} ⊆ X.
+Proof.
+  rewrite elem_of_multiplicity. intros Hx y; destruct (decide (x = y)) as [->|].
+  - rewrite multiplicity_singleton; omega.
+  - rewrite multiplicity_singleton_ne by done; omega.
+Qed.
+
 (* Properties of the elements operation *)
 Lemma gmultiset_elements_empty : elements (∅ : gmultiset A) = [].
 Proof.
-- 
GitLab