diff --git a/theories/gmultiset.v b/theories/gmultiset.v
index ba37efe15c7f10ac1ef8bf0767856f4bda25f3b8..c07aa6c3e93ed6ee150d65a12d723e047b5d00fd 100644
--- a/theories/gmultiset.v
+++ b/theories/gmultiset.v
@@ -370,6 +370,8 @@ Section more_lemmas.
   Proof. multiset_solver. Qed.
 
   (** Element of operation *)
+  Lemma gmultiset_not_elem_of_empty x : x ∉@{gmultiset A} ∅.
+  Proof. multiset_solver. Qed.
   Lemma gmultiset_not_elem_of_singleton x y : x ∉@{gmultiset A} {[+ y +]} ↔ x ≠ y.
   Proof. multiset_solver. Qed.
   Lemma gmultiset_not_elem_of_union x X Y : x ∉ X ∪ Y ↔ x ∉ X ∧ x ∉ Y.