diff --git a/iris/algebra/gmap.v b/iris/algebra/gmap.v
index dc39ca0feb51e4f1d2704ac2ea5c3a16d4e30277..35a53a7317c8c3fdba72a2920a252cd3f9c27bc3 100644
--- a/iris/algebra/gmap.v
+++ b/iris/algebra/gmap.v
@@ -349,6 +349,9 @@ Proof.
     apply Some_included. by rewrite Hi.
   - intros ?. exists y. by rewrite lookup_insert Some_included.
 Qed.
+Lemma singleton_mono i x y :
+  x ≼ y → {[ i := x ]} ≼ ({[ i := y ]} : gmap K A).
+Proof. intros Hincl. apply singleton_included. right. done. Qed.
 
 Global Instance singleton_cancelable i x :
   Cancelable (Some x) → Cancelable {[ i := x ]}.