X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Flibrary%2Fnat%2Fnth_prime.ma;h=e174266e6884f41cfb4fe256cbe83294790096a4;hb=42f43b29d87e84825a3f6a65674dc30cd670333f;hp=5330f52adbb923ddd84fc91ac1a876b373751ccc;hpb=7f2444c2670cadafddd8785b687ef312158376b0;p=helm.git

diff --git a/matita/library/nat/nth_prime.ma b/matita/library/nat/nth_prime.ma
index 5330f52ad..e174266e6 100644
--- a/matita/library/nat/nth_prime.ma
+++ b/matita/library/nat/nth_prime.ma
@@ -41,8 +41,8 @@ qed. *)
 theorem smallest_factor_fact: \forall n:nat.
 n < smallest_factor (S n!).
 intros.
-apply not_le_to_lt.
-change with (smallest_factor (S n!) \le n \to False).intro.
+apply not_le_to_lt.unfold Not.
+intro.
 apply (not_divides_S_fact n (smallest_factor(S n!))).
 apply lt_SO_smallest_factor.
 unfold lt.apply le_S_S.apply le_SO_fact.
@@ -63,8 +63,7 @@ split.split.
 apply smallest_factor_fact.
 apply le_smallest_factor_n.
 (* Andrea: ancora hint non lo trova *)
-apply prime_smallest_factor_n.
-change with ((S(S O)) \le S (S n1)!).
+apply prime_smallest_factor_n.unfold lt.
 apply le_S.apply le_SSO_fact.
 unfold lt.apply le_S_S.assumption.
 qed.
@@ -78,7 +77,7 @@ match n with
     min_aux (upper_bound - (S previous_prime)) upper_bound primeb].
     
 (* it works, but nth_prime 4 takes already a few minutes -
-it must compute factorial of 7 ...
+it must compute factorial of 7 ...*)
 
 theorem example11 : nth_prime (S(S O)) = (S(S(S(S(S O))))).
 normalize.reflexivity.
@@ -90,12 +89,16 @@ qed.
 
 theorem example13 : nth_prime (S(S(S(S O)))) = (S(S(S(S(S(S(S(S(S(S(S O))))))))))).
 normalize.reflexivity.
+qed.
+
+(*
+theorem example14 : nth_prime (S(S(S(S(S O))))) = (S(S(S(S(S(S(S(S(S(S(S O))))))))))).
+normalize.reflexivity.
 *) 
 
 theorem prime_nth_prime : \forall n:nat.prime (nth_prime n).
 intro.
-apply (nat_case n).
-change with (prime (S(S O))).
+apply (nat_case n).simplify.
 apply (primeb_to_Prop (S(S O))).
 intro.
 change with
@@ -115,14 +118,13 @@ apply le_S_S.
 apply le_n_fact_n.
 apply le_smallest_factor_n.
 apply prime_to_primeb_true.
-apply prime_smallest_factor_n.
-change with ((S(S O)) \le S (nth_prime m)!).
+apply prime_smallest_factor_n.unfold lt.
 apply le_S_S.apply le_SO_fact.
 qed.
 
 (* properties of nth_prime *)
 theorem increasing_nth_prime: increasing nth_prime.
-change with (\forall n:nat. (nth_prime n) < (nth_prime (S n))).
+unfold increasing.
 intros.
 change with
 (let previous_prime \def (nth_prime n) in