diff --git a/theories/algebra/cmra.v b/theories/algebra/cmra.v
index 115ba5c5051fb6b73fa2e8563dc87bb77df85a76..b4aaea2c921d8813ff7faec0d898f5c898d0965b 100644
--- a/theories/algebra/cmra.v
+++ b/theories/algebra/cmra.v
@@ -1430,6 +1430,14 @@ Section option_prod.
   Proof. intros ?%Some_pair_included. by rewrite -(Some_included_total b1). Qed.
 End option_prod.
 
+Lemma option_fmap_mono {A B : cmraT} (f : A → B) ma mb :
+  Proper ((≡) ==> (≡)) f →
+  (∀ a b, a ≼ b → f a ≼ f b) →
+  ma ≼ mb → f <$> ma ≼ f <$> mb.
+Proof.
+  intros ??. rewrite !option_included; intros [->|(a&b&->&->&?)]; naive_solver.
+Qed.
+
 Instance option_fmap_cmra_morphism {A B : cmraT} (f: A → B) `{!CmraMorphism f} :
   CmraMorphism (fmap f : option A → option B).
 Proof.
diff --git a/theories/algebra/gmap.v b/theories/algebra/gmap.v
index 59230337296832a37a64068723e2ca9d3970672e..1ae544dbc013992eb418e9407de87cb33e5447ce 100644
--- a/theories/algebra/gmap.v
+++ b/theories/algebra/gmap.v
@@ -474,6 +474,14 @@ Proof.
   apply (delete_local_update_cancelable m _ i (Some x));
     [done|by rewrite lookup_singleton].
 Qed.
+
+Lemma gmap_fmap_mono {B : ucmraT} (f : A → B) m1 m2 :
+  Proper ((≡) ==> (≡)) f →
+  (∀ x y, x ≼ y → f x ≼ f y) → m1 ≼ m2 → fmap f m1 ≼ fmap f m2.
+Proof.
+  intros ??. rewrite !lookup_included=> Hm i.
+  rewrite !lookup_fmap. by apply option_fmap_mono.
+Qed.
 End properties.
 
 Section unital_properties.