From 18c543b35ec63710b2f090d91632ac84b6474d2b Mon Sep 17 00:00:00 2001
From: Michael Sammler <noreply@sammler.me>
Date: Mon, 8 Aug 2022 16:35:18 +0200
Subject: [PATCH] Add some _1, _2 lemmas

---
 theories/fin_maps.v | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index 6331dde7..ba503b2e 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -1385,6 +1385,14 @@ Section map_filter.
     - intros Hm i. destruct (m !! i) as [x|] eqn:?; [|by auto].
       right; intros ? [= <-]. by apply Hm.
   Qed.
+  Lemma map_filter_empty_iff_1 m :
+    filter P m = ∅ →
+    map_Forall (λ i x, ¬P (i,x)) m.
+  Proof. apply map_filter_empty_iff. Qed.
+  Lemma map_filter_empty_iff_2 m :
+    map_Forall (λ i x, ¬P (i,x)) m →
+    filter P m = ∅.
+  Proof. apply map_filter_empty_iff. Qed.
 
   Lemma map_filter_delete m i : filter P (delete i m) = delete i (filter P m).
   Proof.
-- 
GitLab