diff --git a/algebra/dec_agree.v b/algebra/dec_agree.v
index b21ef80449274ae1aec88b7f870e41b84030b4b7..b11932e59a78ac8c3a5bb3fd01e0d0c13329f5bc 100644
--- a/algebra/dec_agree.v
+++ b/algebra/dec_agree.v
@@ -45,6 +45,9 @@ Qed.
 Canonical Structure dec_agreeR : cmraT := discreteR dec_agree_ra.
 
 (* Some properties of this CMRA *)
+Lemma dec_agree_core_id (x : dec_agree A) : core x = x.
+Proof. done. Qed.
+
 Lemma dec_agree_ne a b : a ≠ b → DecAgree a ⋅ DecAgree b = DecAgreeBot.
 Proof. intros. by rewrite /= decide_False. Qed.