diff --git a/theories/list.v b/theories/list.v
index b73ac068bf9542e1a4eec264ea44aa630ec0732b..fb2339c8d12ae162c5ccf9e0b9540985df3e6284 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -1971,6 +1971,19 @@ Section filter.
     intros [k ->]%elem_of_Permutation ?; simpl.
     rewrite decide_False, Nat.lt_succ_r by done. apply filter_length.
   Qed.
+  Lemma not_elem_of_filter_nil `{EqDecision A} l x :
+    filter P l = [] → P x → x ∉ l.
+  Proof.
+    intros Hfilter HP Hin.
+    induction l as [|y l IHl]; [by inversion Hin|].
+    destruct (decide (x = y)) as [<-|Hneq].
+    { by rewrite filter_cons_True in Hfilter. }
+    apply elem_of_cons in Hin.
+    destruct Hin as [<-|Hin]; [done|].
+    destruct (decide (P y)); [by rewrite filter_cons_True in Hfilter|].
+    apply IHl; [|done]. by rewrite filter_cons_False in Hfilter.
+  Qed.
+
 End filter.
 
 Lemma list_filter_iff (P1 P2 : A → Prop)