Add lemmas for big_opS and gmap singletons

This is a particular pattern that comes up in the lifetime logic which I
want to be able to rewrite, which is why I've extracted it to a general
lemma.

iris/algebra/gmap.v

@@ -672,6 +672,21 @@ Proof.
   rewrite insert_singleton_op ?not_elem_of_list_to_map_1 //.
 Qed.
 
+Lemma big_opS_gset_to_gmap (X : gset K) (a : A) :
+  ([^op set] x ∈ X, {[ x := a ]}) ≡ gset_to_gmap a X.
+Proof.
+  induction X as [|? ? ? IHX] using set_ind_L.
+  { intros ?; rewrite big_opS_empty gset_to_gmap_empty //=. }
+  rewrite big_opS_insert //.
+  rewrite gset_to_gmap_union_singleton.
+  rewrite insert_singleton_op; [|by rewrite lookup_gset_to_gmap_None].
+  by rewrite IHX.
+Qed.
+
+Lemma big_opS_gset_to_gmap_L `{!LeibnizEquiv A} (X : gset K) (a : A) :
+  ([^op set] x ∈ X, {[ x := a ]}) = gset_to_gmap a X.
+Proof. apply leibniz_equiv, big_opS_gset_to_gmap. Qed.
+
 End properties.
 
 Section unital_properties.