proposition: Lemma Injective_carac A B (l:list A) : Listing l -> forall (f:A->B), Injective f <-> NoDup (map f l).
proof: Proof. intros L f. split. - intros Ij. apply Injective_map_NoDup; trivial. apply L. - intros N x y E. assert (X : In x l) by apply L. assert (Y : In y l) by apply L. apply In_nth_error in X. destruct X as (i,X). apply In_nth_error in Y. destruct Y as (j,Y). assert (X' := map_nth_error f _ _ X). assert (Y' := map_nth_error f _ _ Y). assert (i = j). { rewrite NoDup_nth_error in N. apply N. - rewrite <- nth_error_Some. now rewrite X'. - rewrite X', Y'. now f_equal. } subst j. rewrite Y in X. now injection X. Qed.
imports: List PeanoNat Compare_dec EqNat Decidable ListDec