diff --git a/theories/algebra/gmap.v b/theories/algebra/gmap.v
index ed15a0559722da3c6c6608a769379748a2bd1870..c2de82129516c4797ca5ef170a09cd1bfda2e5d5 100644
--- a/theories/algebra/gmap.v
+++ b/theories/algebra/gmap.v
@@ -594,6 +594,15 @@ Proof.
   intros ??. rewrite !lookup_included=> Hm i.
   rewrite !lookup_fmap. by apply option_fmap_mono.
 Qed.
+
+Lemma big_opM_singletons (m : gmap K A) :
+  ([^op map] k ↦ x ∈ m, {[ k := x ]}) ≡ m.
+Proof.
+  induction m as [|k x m Hk IH] using map_ind.
+  - rewrite big_opM_empty. done.
+  - rewrite big_opM_insert // IH insert_singleton_op //.
+Qed.
+
 End properties.
 
 Section unital_properties.