integration of statements for NoDup

1 files changed, 15 insertions, 0 deletions

diff --git a/theories/Lists/List.v b/theories/Lists/List.v
index d7d7dbb5c5..c6dffe92c9 100644
--- a/theories/Lists/List.v
+++ b/theories/Lists/List.v
@@ -2306,6 +2306,16 @@ Section ReDun.
     + now constructor.
   Qed.
 
+  Lemma NoDup_rev l : NoDup l -> NoDup (rev l).
+  Proof.
+    induction l; simpl; intros Hnd; [ constructor | ].
+    inversion_clear Hnd as [ | ? ? Hnin Hndl ].
+    assert (Add a (rev l) (rev l ++ a :: nil)) as Hadd
+      by (rewrite <- (app_nil_r (rev l)) at 1; apply Add_app).
+    apply NoDup_Add in Hadd; apply Hadd; intuition.
+    now apply Hnin, in_rev.
+  Qed.
+
   (** Effective computation of a list without duplicates *)
 
   Hypothesis decA: forall x y : A, {x = y} + {x <> y}.
@@ -2334,6 +2344,11 @@ Section ReDun.
       * reflexivity.
   Qed.
 
+  Lemma nodup_incl l1 l2 : incl l1 (nodup l2) <-> incl l1 l2.
+  Proof.
+    split; intros Hincl a Ha; apply nodup_In; intuition.
+  Qed.
+
   Lemma NoDup_nodup l: NoDup (nodup l).
   Proof.
     induction l as [|a l' Hrec]; simpl.