* Obsolete debugging comments removed

[helm.git] / helm / matita / library / nat / nth_prime.ma

diff --git a/helm/matita/library/nat/nth_prime.ma b/helm/matita/library/nat/nth_prime.ma
index 5ff937e42b139a94f281cddb19aa6872a968ba2f..200ccba5a9086b0ca2a940c7f19ae0964bb8402c 100644 (file)
--- a/helm/matita/library/nat/nth_prime.ma
+++ b/helm/matita/library/nat/nth_prime.ma
@@ -15,6 +15,7 @@
 set "baseuri" "cic:/matita/nat/nth_prime".
 
 include "nat/primes.ma".
+include "nat/lt_arith.ma".
 
 (* upper bound by Bertrand's conjecture. *)
 (* Too difficult to prove.        
@@ -42,17 +43,16 @@ n < smallest_factor (S (fact n)).
 intros.
 apply not_le_to_lt.
 change with smallest_factor (S (fact n)) \le n \to False.intro.
-apply not_divides_S_fact n (smallest_factor(S (fact n))) ? ?.
-apply divides_smallest_factor_n.
-simplify.apply le_S_S.apply le_O_n.
+apply not_divides_S_fact n (smallest_factor(S (fact n))).
 apply lt_SO_smallest_factor.
 simplify.apply le_S_S.apply le_SO_fact.
 assumption.
+apply divides_smallest_factor_n.
+simplify.apply le_S_S.apply le_O_n.
 qed.
 
-(* mi sembra che il problem sia ex *)
-theorem ex_prime: \forall n. (S O) \le n \to ex nat (\lambda m.
-n < m \land m \le (S (fact n)) \land (prime m)).
+theorem ex_prime: \forall n. (S O) \le n \to \exists m.
+n < m \land m \le (S (fact n)) \land (prime m).
 intros.
 elim H.
 apply ex_intro nat ? (S(S O)).
@@ -62,7 +62,7 @@ apply ex_intro nat ? (smallest_factor (S (fact (S n1)))).
 split.split.
 apply smallest_factor_fact.
 apply le_smallest_factor_n.
-(* ancora hint non lo trova *)
+(* Andrea: ancora hint non lo trova *)
 apply prime_smallest_factor_n.
 change with (S(S O)) \le S (fact (S n1)).
 apply le_S.apply le_SSO_fact.
@@ -98,7 +98,6 @@ apply nat_case n.
 change with prime (S(S O)).
 apply primeb_to_Prop (S(S O)).
 intro.
-(* ammirare la resa del letin !! *)
 change with
 let previous_prime \def (nth_prime m) in
 let upper_bound \def S (fact previous_prime) in
@@ -162,7 +161,7 @@ qed.
 
 theorem ex_m_le_n_nth_prime_m: 
 \forall n: nat. nth_prime O \le n \to 
-ex nat (\lambda m. nth_prime m \le n \land n < nth_prime (S m)).
+\exists m. nth_prime m \le n \land n < nth_prime (S m).
 intros.
 apply increasing_to_le2.
 exact lt_nth_prime_n_nth_prime_Sn.assumption.
@@ -187,9 +186,9 @@ qed.
 
 (* nth_prime enumerates all primes *)
 theorem prime_to_nth_prime : \forall p:nat. prime p \to
-ex nat (\lambda i:nat. nth_prime i = p).
+\exists i. nth_prime i = p.
 intros.
-cut ex nat (\lambda m. nth_prime m \le p \land p < nth_prime (S m)).
+cut \exists m. nth_prime m \le p \land p < nth_prime (S m).
 elim Hcut.elim H1.
 cut nth_prime a < p \lor nth_prime a = p.
 elim Hcut1.