diff --git a/theories/gmultiset.v b/theories/gmultiset.v
index 51b1a9831c582f61474e9ab734bef50b86c31bce..0fab06bc05343dfdbd8759b4e2b3e607c75649b0 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.