diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index d53ea3249f4049fdf8bbf37063a8464c3abf6cee..bcce9efdf60f708d6e280c38d4f259ecd2c7c46a 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -1884,6 +1884,11 @@ Proof.
   destruct (m1 !! i) as [x'|], (m2 !! i);
     try specialize (Hm1m2 x'); compute; intuition congruence.
 Qed.
+Lemma map_difference_diag {A} (m : M A) : m ∖ m = ∅.
+Proof.
+  apply map_empty; intros i. rewrite lookup_difference_None.
+  destruct (m !! i); eauto.
+Qed.
 End theorems.
 
 (** * Tactics *)