diff --git a/modures/cmra.v b/modures/cmra.v
index d0abf150acc79f3901a2223e8f9466ceb4d0eabf..4c43104751729d221b344ccb2d57989b43357c7c 100644
--- a/modures/cmra.v
+++ b/modures/cmra.v
@@ -327,6 +327,20 @@ Proof.
 Qed.
 Lemma ra_updateP_weaken (P Q : A → Prop) x : x ⇝: P → (∀ y, P y → Q y) → x ⇝: Q.
 Proof. eauto using ra_updateP_compose, ra_updateP_id. Qed.
+
+Lemma ra_updateP_op (P1 P2 Q : A → Prop) x1 x2 :
+  x1 ⇝: P1 → x2 ⇝: P2 → (∀ y1 y2, P1 y1 → P2 y2 → Q (y1 ⋅ y2)) → x1 ⋅ x2 ⇝: Q.
+Proof.
+  intros Hx1 Hx2 Hy z n ?.
+  destruct (Hx1 (x2 â‹… z) n) as (y1&?&?); first by rewrite associative.
+  destruct (Hx2 (y1 â‹… z) n) as (y2&?&?);
+    first by rewrite associative (commutative _ x2) -associative.
+  exists (y1 â‹… y2); split; last rewrite (commutative _ y1) -associative; auto.
+Qed.
+Lemma ra_update_op x1 x2 y1 y2 : x1 ⇝ y1 → x2 ⇝ y2 → x1 ⋅ x2 ⇝ y1 ⋅ y2.
+Proof.
+  rewrite !cmra_update_updateP; eauto using ra_updateP_op with congruence.
+Qed.
 End cmra.
 
 Hint Extern 0 (_ ≼{0} _) => apply cmra_includedN_0.