diff --git a/algebra/cmra_big_op.v b/algebra/cmra_big_op.v
index 993c58ff5d55e8e3a64d8d877f7d95f3fbd7091d..f0aeaf98528c98adf8863793f2f0cbba14263bd6 100644
--- a/algebra/cmra_big_op.v
+++ b/algebra/cmra_big_op.v
@@ -452,6 +452,16 @@ Section gmultiset.
     intros. by rewrite /big_opMS gmultiset_elements_singleton /= right_id.
   Qed.
 
+  Lemma big_opMS_delete f X x :
+    x ∈ X → ([⋅ mset] y ∈ X, f y) ≡ f x ⋅ [⋅ mset] y ∈ X ∖ {[ x ]}, f y.
+  Proof.
+    intros ?%gmultiset_elem_of_subseteq. rewrite -big_opMS_singleton.
+    by rewrite -big_opMS_union -gmultiset_union_difference.
+  Qed.
+
+  Lemma big_opMS_elem_of f X x : x ∈ X → f x ≼ [⋅ mset] y ∈ X, f y.
+  Proof. intros. rewrite big_opMS_delete //. apply cmra_included_l. Qed.
+
   Lemma big_opMS_opS f g X :
     ([⋅ mset] y ∈ X, f y ⋅ g y) ≡ ([⋅ mset] y ∈ X, f y) ⋅ ([⋅ mset] y ∈ X, g y).
   Proof.
diff --git a/prelude/gmultiset.v b/prelude/gmultiset.v
index 67e2a4aabcf74b53494bedbc03ae53e45e85fcff..9767b9a460a773ea58b88ea586b0cc95700bdfc4 100644
--- a/prelude/gmultiset.v
+++ b/prelude/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.