proposition: Lemma NoDup_nth_error l : NoDup l <-> (forall i j, i<length l -> nth_error l i = nth_error l j -> i = j).
proof: Proof. split. { intros H; induction H as [|a l Hal Hl IH]; intros i j Hi E. - inversion Hi. - destruct i, j; simpl in *; auto. * elim Hal. eapply nth_error_In; eauto. * elim Hal. eapply nth_error_In; eauto. * f_equal. now apply IH;[apply Nat.succ_lt_mono|]. } { induction l as [|a l IHl]; intros H; constructor. * intro Ha. apply In_nth_error in Ha. destruct Ha as (n,Hn). assert (n < length l) by (now rewrite <- nth_error_Some, Hn). specialize (H 0 (S n)). simpl in H. now discriminate H; [apply Nat.lt_0_succ|]. * apply IHl. intros i j Hi %Nat.succ_lt_mono E. now apply eq_add_S, H. } Qed.
imports: PeanoNat