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

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

diff --git a/helm/matita/library/nat/orders.ma b/helm/matita/library/nat/orders.ma
index 1731f2bc2e8ac3973d28255d61c04be3df060e36..71cd5945037fe43fe3d9dbdef3a8ae5fd5770186 100644 (file)
--- a/helm/matita/library/nat/orders.ma
+++ b/helm/matita/library/nat/orders.ma
@@ -282,7 +282,7 @@ simplify in H. apply H.
 qed.
 
 theorem increasing_to_le: \forall f:nat \to nat. (increasing f) 
-\to \forall m:nat. ex nat (\lambda i. m \le (f i)).
+\to \forall m:nat. \exists i. m \le (f i).
 intros.elim m.
 apply ex_intro ? ? O.apply le_O_n.
 elim H1.
@@ -295,7 +295,7 @@ qed.
 
 theorem increasing_to_le2: \forall f:nat \to nat. (increasing f) 
 \to \forall m:nat. (f O) \le m \to 
-ex nat (\lambda i. (f i) \le m \land m <(f (S i))).
+\exists i. (f i) \le m \land m <(f (S i)).
 intros.elim H1.
 apply ex_intro ? ? O.
 split.apply le_n.apply H.