From a727a79758f5073eebcbf8ed146eeb6b541b3415 Mon Sep 17 00:00:00 2001
From: Jonas Kastberg Hinrichsen <jihgfee@gmail.com>
Date: Wed, 12 Jan 2022 14:51:31 +0100
Subject: [PATCH] Added a useful lemma about [filter] on list

---
 theories/list.v | 13 +++++++++++++
 1 file changed, 13 insertions(+)

diff --git a/theories/list.v b/theories/list.v
index b73ac068..fb2339c8 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)
-- 
GitLab