More big_opMS lemmas.

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.

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.