Notation for "ex" introduced. It is the same as the notation for forall,

[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 0b8f2bbe207f38580c466e45152f7cffc88cbbb2..8035d49ddba64dcb5d207ab2e4c9179d477d4d2c 100644 (file)
--- a/helm/matita/library/nat/nth_prime.ma
+++ b/helm/matita/library/nat/nth_prime.ma
@@ -51,9 +51,8 @@ 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)).
@@ -163,7 +162,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.
@@ -188,9 +187,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.