qed.
(* general properties of functions *)
theorem monotonic_to_injective: \forall f:nat\to nat.
monotonic nat lt f \to injective nat nat f.
qed.
(* general properties of functions *)
theorem monotonic_to_injective: \forall f:nat\to nat.
monotonic nat lt f \to injective nat nat f.
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.
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.