Prove that `fmap` on `option` and `gmap` is monotone.

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.

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.