add _singletons lemmas for big_opMS and big_opS

theories/algebra/gmultiset.v

 From stdpp Require Export sets gmultiset countable.
 From iris.algebra Require Export cmra.
-From iris.algebra Require Import updates local_updates.
+From iris.algebra Require Import updates local_updates big_op.
 From iris Require Import options.
 
 (* The multiset union CMRA *)
@@ -81,6 +81,15 @@ Section gmultiset.
     repeat (rewrite multiplicity_difference || rewrite multiplicity_disj_union).
     lia.
   Qed.
+
+  Lemma big_opMS_singletons X :
+    ([^op mset] x ∈ X, {[ x ]}) = X.
+  Proof.
+    induction X as [|x X IH] using gmultiset_ind.
+    - rewrite big_opMS_empty. done.
+    - unfold_leibniz. rewrite big_opMS_disj_union // big_opMS_singleton IH //.
+  Qed.
+
 End gmultiset.
 
 Arguments gmultisetO _ {_ _}.

theories/algebra/gset.v

 From stdpp Require Export sets gmap mapset.
 From iris.algebra Require Export cmra.
-From iris.algebra Require Import updates local_updates.
+From iris.algebra Require Import updates local_updates big_op.
 From iris Require Import options.
 
 (* The union CMRA *)
@@ -55,6 +55,15 @@ Section gset.
 
   Global Instance gset_core_id X : CoreId X.
   Proof. by apply core_id_total; rewrite gset_core_self. Qed.
+
+  Lemma big_opS_singletons X :
+    ([^op set] x ∈ X, {[ x ]}) = X.
+  Proof.
+    induction X as [|x X Hx IH] using set_ind_L.
+    - rewrite big_opS_empty. done.
+    - unfold_leibniz. rewrite big_opS_insert // IH //.
+  Qed.
+
 End gset.
 
 Arguments gsetO _ {_ _}.