diff --git a/iris/algebra/updates.v b/iris/algebra/updates.v
index 9807071cecf49fa053fe91e3e8834eb446bee2dc..1f5401ff8415bb28bedaaaf8c47f80043991b799 100644
--- a/iris/algebra/updates.v
+++ b/iris/algebra/updates.v
@@ -107,6 +107,9 @@ Proof. intros n mz. rewrite comm cmra_op_opM_assoc. apply cmra_validN_op_r. Qed.
 Lemma cmra_update_op_r x y : x â‹… y ~~> y.
 Proof. rewrite comm. apply cmra_update_op_l. Qed.
 
+Lemma cmra_update_included x y : x ≼ y → y ~~> x.
+Proof. intros [z ->]. apply cmra_update_op_l. Qed.
+
 Lemma cmra_update_valid0 x y : (✓{0} x → x ~~> y) → x ~~> y.
 Proof.
   intros H n mz Hmz. apply H, Hmz.