diff --git a/algebra/cmra.v b/algebra/cmra.v
index 41e9c043712605a6f14293812b6e3b3f90dfdaf0..93ee00523cddf35139e7f2a6e0c5142c77394a8c 100644
--- a/algebra/cmra.v
+++ b/algebra/cmra.v
@@ -344,6 +344,10 @@ Lemma exclusive_r x `{!Exclusive x} y : ✓ (y ⋅ x) → False.
 Proof. rewrite comm. by apply exclusive_l. Qed.
 Lemma exclusiveN_opM n x `{!Exclusive x} my : ✓{n} (x ⋅? my) → my = None.
 Proof. destruct my as [y|]. move=> /(exclusiveN_l _ x) []. done. Qed.
+Lemma exclusive_includedN n x `{!Exclusive x} y : x ≼{n} y → ✓{n} y → False.
+Proof. intros [? ->]. by apply exclusiveN_l. Qed.
+Lemma exclusive_included x `{!Exclusive x} y : x ≼ y → ✓ y → False.
+Proof. intros [? ->]. by apply exclusive_l. Qed.
 
 (** ** Order *)
 Lemma cmra_included_includedN n x y : x ≼ y → x ≼{n} y.