+(* div *)
+
+theorem eq_mod_O_to_lt_O_div: \forall n,m:nat. O < m \to O < n\to n \mod m = O \to O < n / m.
+intros 4.apply (lt_O_n_elim m H).intros.
+apply (lt_times_to_lt_r m1).
+rewrite < times_n_O.
+rewrite > (plus_n_O ((S m1)*(n / (S m1)))).
+rewrite < H2.
+rewrite < sym_times.
+rewrite < div_mod.
+rewrite > H2.
+assumption.
+unfold lt.apply le_S_S.apply le_O_n.
+qed.
+
+theorem lt_div_n_m_n: \forall n,m:nat. (S O) < m \to O < n \to n / m \lt n.
+intros.
+apply (nat_case1 (n / m)).intro.
+assumption.intros.rewrite < H2.
+rewrite > (div_mod n m) in \vdash (? ? %).
+apply (lt_to_le_to_lt ? ((n / m)*m)).
+apply (lt_to_le_to_lt ? ((n / m)*(S (S O)))).
+rewrite < sym_times.
+rewrite > H2.
+simplify.unfold lt.
+rewrite < plus_n_O.
+rewrite < plus_n_Sm.
+apply le_S_S.
+apply le_S_S.
+apply le_plus_n.
+apply le_times_r.
+assumption.
+rewrite < sym_plus.
+apply le_plus_n.
+apply (trans_lt ? (S O)).
+unfold lt. apply le_n.assumption.
+qed.
+
+(* general properties of functions *)
+theorem monotonic_to_injective: \forall f:nat\to nat.
+monotonic nat lt f \to injective nat nat f.
+unfold injective.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.
+intros.assumption.
+intro.apply False_ind.apply (not_le_Sn_n (f y)).
+rewrite < H1 in \vdash (? ? %).apply H.apply H2.
+qed.
+
+theorem increasing_to_injective: \forall f:nat\to nat.
+increasing f \to injective nat nat f.
+intros.apply monotonic_to_injective.
+apply increasing_to_monotonic.assumption.
+qed.