proposition: Lemma inj_nth_nodup (x : A) l i j : nodup l -> i < length l -> j < length l -> nth i l x = nth j l x -> i = j.
proof: Proof. intros hl hi hj. gen (nth_In x hi). set (a := nth i l x). intros h e. destruct (In_nodup_elim h hl) as [l1 [l2 [n0 [n1 n2]]]]. rewrite n0, app_length in hi, hj. simpl in hi, hj. destruct (lt_dec j (length l1)). assert (aj : a = nth j l1 x). rewrite e, n0, app_nth1; auto. gen (nth_In x l0). rewrite <- aj. tauto. assert (aj : a = nth (j-length l1) (a::l2) x). rewrite e at 1. rewrite n0, app_nth2. refl. lia. destruct (lt_dec i (length l1)). assert (ai : a = nth i l1 x). unfold a. rewrite n0, app_nth1; auto. gen (nth_In x l0). rewrite <- ai. tauto. assert (ai : a = nth (i-length l1) (a::l2) x). unfold a at 1. rewrite n0, app_nth2. refl. lia. gen aj. gen ai. simpl. case_eq (j - length l1). case_eq (i - length l1). intros; lia. intros r r1 r2 _ r3. assert (p : r < length l2). lia. gen (nth_In x p). simpl in ai. rewrite r1 in ai. rewrite <- ai. tauto. intros r r1. assert (p : r < length l2). lia. gen (nth_In x p). simpl in aj. rewrite r1 in aj. rewrite <- aj. tauto. Qed.
imports: CoLoR(ListUtil NatUtil RelMidex LogicUtil)