X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Flibrary%2Fnat%2Fnth_prime.ma;h=5330f52adbb923ddd84fc91ac1a876b373751ccc;hb=97c2d258a5c524eb5c4b85208899d80751a2c82f;hp=5fa636301425eb1354b40403b374c54e860134f1;hpb=fb94e5a71be508516514dfe50528ccfb3cd2da91;p=helm.git

diff --git a/helm/matita/library/nat/nth_prime.ma b/helm/matita/library/nat/nth_prime.ma
index 5fa636301..5330f52ad 100644
--- a/helm/matita/library/nat/nth_prime.ma
+++ b/helm/matita/library/nat/nth_prime.ma
@@ -45,10 +45,10 @@ apply not_le_to_lt.
 change with (smallest_factor (S n!) \le n \to False).intro.
 apply (not_divides_S_fact n (smallest_factor(S n!))).
 apply lt_SO_smallest_factor.
-simplify.apply le_S_S.apply le_SO_fact.
+unfold lt.apply le_S_S.apply le_SO_fact.
 assumption.
 apply divides_smallest_factor_n.
-simplify.apply le_S_S.apply le_O_n.
+unfold lt.apply le_S_S.apply le_O_n.
 qed.
 
 theorem ex_prime: \forall n. (S O) \le n \to \exists m.
@@ -66,7 +66,7 @@ apply le_smallest_factor_n.
 apply prime_smallest_factor_n.
 change with ((S(S O)) \le S (S n1)!).
 apply le_S.apply le_SSO_fact.
-simplify.apply le_S_S.assumption.
+unfold lt.apply le_S_S.assumption.
 qed.
 
 let rec nth_prime n \def
@@ -147,14 +147,14 @@ apply increasing_nth_prime.
 qed.
 
 theorem lt_SO_nth_prime_n : \forall n:nat. (S O) \lt nth_prime n.
-intros. elim n.simplify.apply le_n.
+intros. elim n.unfold lt.apply le_n.
 apply (trans_lt ? (nth_prime n1)).
 assumption.apply lt_nth_prime_n_nth_prime_Sn.
 qed.
 
 theorem lt_O_nth_prime_n : \forall n:nat. O \lt nth_prime n.
 intros.apply (trans_lt O (S O)).
-simplify. apply le_n.apply lt_SO_nth_prime_n.
+unfold lt. apply le_n.apply lt_SO_nth_prime_n.
 qed.
 
 theorem ex_m_le_n_nth_prime_m: 
@@ -195,6 +195,6 @@ apply (lt_nth_prime_to_not_prime a).assumption.assumption.
 apply (ex_intro nat ? a).assumption.
 apply le_to_or_lt_eq.assumption.
 apply ex_m_le_n_nth_prime_m.
-simplify.simplify in H.elim H.assumption.
+simplify.unfold prime in H.elim H.assumption.
 qed.