\forall n:nat.monotonic nat lt (\lambda m.n+m).
simplify.intros.
elim n.simplify.assumption.
-simplify.
+simplify.unfold lt.
apply le_S_S.assumption.
qed.
rewrite > plus_n_O.
rewrite > (plus_n_O q).assumption.
apply H.
-simplify.apply le_S_S_to_le.
+unfold lt.apply le_S_S_to_le.
rewrite > plus_n_Sm.
rewrite > (plus_n_Sm q).
exact H1.
(* times and zero *)
theorem lt_O_times_S_S: \forall n,m:nat.O < (S n)*(S m).
-intros.simplify.apply le_S_S.apply le_O_n.
+intros.simplify.unfold lt.apply le_S_S.apply le_O_n.
qed.
(* times *)
rewrite < div_mod.
rewrite > H2.
assumption.
-simplify.apply le_S_S.apply le_O_n.
+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.
apply (lt_to_le_to_lt ? ((n / m)*(S (S O)))).
rewrite < sym_times.
rewrite > H2.
-simplify.
+simplify.unfold lt.
rewrite < plus_n_O.
rewrite < plus_n_Sm.
apply le_S_S.
rewrite < sym_plus.
apply le_plus_n.
apply (trans_lt ? (S O)).
-simplify. apply le_n.assumption.
+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.
-simplify.intros.
+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.