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.