-simplify.intros.
-apply nat_compare_elim x y.
-intro.apply False_ind.apply not_le_Sn_n (f x).
-rewrite > H1 in \vdash (? ? %).apply H.apply H2.
+unfold injective.intros.
+apply (nat_compare_elim x y).
+intro.apply False_ind.apply (not_le_Sn_n (f x)).
+rewrite > H1 in \vdash (? ? %).
+change with (f x < f y).
+apply H.apply H2.