additional statements on flat_map

1 files changed, 15 insertions, 0 deletions

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. *)