X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Flibrary%2Fnat%2Flt_arith.ma;h=b8339f374e6019dd054719c9928bf735c63aef4b;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=4897fb59875a8d8968e122f44ca66b59e9994870;hpb=fb94e5a71be508516514dfe50528ccfb3cd2da91;p=helm.git

diff --git a/helm/matita/library/nat/lt_arith.ma b/helm/matita/library/nat/lt_arith.ma
index 4897fb598..b8339f374 100644
--- a/helm/matita/library/nat/lt_arith.ma
+++ b/helm/matita/library/nat/lt_arith.ma
@@ -21,7 +21,7 @@ theorem monotonic_lt_plus_r:
 \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.
 
@@ -51,7 +51,7 @@ intro.elim n.
 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.
@@ -65,7 +65,7 @@ qed.
 
 (* 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 *)
@@ -172,7 +172,7 @@ rewrite < sym_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.
@@ -184,7 +184,7 @@ 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.
+simplify.unfold lt.
 rewrite < plus_n_O.
 rewrite < plus_n_Sm.
 apply le_S_S.
@@ -195,13 +195,13 @@ assumption.
 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.