diff --git a/theories/collections.v b/theories/collections.v
index 88daad82ca17670cc4b7fd7655136aad3f7a98a2..db4d470ec4760e04b0b4f7daf0a89038fac32a0d 100644
--- a/theories/collections.v
+++ b/theories/collections.v
@@ -807,6 +807,8 @@ Section fresh.
     apply IH. by rewrite E.
   Qed.
 
+  Lemma exist_fresh X : ∃ x, x ∉ X.
+  Proof. exists (fresh X). apply is_fresh. Qed.
   Lemma Forall_fresh_NoDup X xs : Forall_fresh X xs → NoDup xs.
   Proof. induction 1; by constructor. Qed.
   Lemma Forall_fresh_elem_of X xs x : Forall_fresh X xs → x ∈ xs → x ∉ X.