proposition: Lemma NotNoDupDup {A : Type} : forall (l : list A), (forall x y : A, {x = y} + {x <> y}) -> ~ NoDup l-> exists e l1 l2, l = l1 ++ e :: l2 /\ In e (l1 ++ l2).
proof: Proof. intros l HDec. induction l; intro HDup. assert (H := NoDup_nil A). contradiction. assert (HIn := in_dec HDec a l). elim HIn; clear HIn; intro HIn. exists a; exists nil; exists l. simpl. auto. assert (HDup' := NoDup_dec l HDec). elim HDup'; clear HDup'; intro HDup'. exfalso. apply HDup. apply NoDup_cons; assumption. apply IHl in HDup'. clear HDec; clear HDup; clear HIn. destruct HDup' as [e [l1 [l2 [HEq HIn]]]]; clear IHl. exists e; exists (a :: l1); exists l2. simpl. split. rewrite HEq; reflexivity. right; assumption. Qed.
imports: Arith NArith List Sorting Coq.Program.Equality