From 73e1dd6f9f936b25c9243719c6f075846beb2c33 Mon Sep 17 00:00:00 2001
From: Olivier Laurent
Date: Fri, 6 Dec 2019 14:11:58 +0100
Subject: additional statements on flat_map

---
 theories/Lists/List.v | 15 +++++++++++++++
 1 file changed, 15 insertions(+)

diff --git a/theories/Lists/List.v b/theories/Lists/List.v
index c1b2c45a8f..729ec7fa34 100644
--- a/theories/Lists/List.v
+++ b/theories/Lists/List.v
@@ -2933,6 +2933,21 @@ Proof.
     now apply IHl.
 Qed.
 
+Lemma in_flat_map_Exists A B : forall (f : A -> list B) x l,
+  In x (flat_map f l) <-> Exists (fun y => In x (f y)) l.
+Proof.
+  intros f x l; rewrite in_flat_map.
+  split; apply Exists_exists.
+Qed.
+
+Lemma notin_flat_map_Forall A B : forall (f : A -> list B) x l,
+  ~ In x (flat_map f l) <-> Forall (fun y => ~ In x (f y)) l.
+Proof.
+  intros f x l; rewrite Forall_Exists_neg.
+  apply not_iff_compat, in_flat_map_Exists.
+Qed.
+
+
 Section Forall2.
 
   (** [Forall2]: stating that elements of two lists are pairwise related. *)
-- 
cgit v1.2.3