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

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

diff --git a/helm/matita/library/nat/factorization.ma b/helm/matita/library/nat/factorization.ma
index 4628eca13c1d86f1f545f95784b118f814b4832b..c8127a1fa8cde6467be67ca32b6549466b56a566 100644 (file)
--- a/helm/matita/library/nat/factorization.ma
+++ b/helm/matita/library/nat/factorization.ma
@@ -29,7 +29,7 @@ divides (nth_prime (max_prime_factor n)) n.
 intros.apply divides_b_true_to_divides.
 apply lt_O_nth_prime_n.
 apply f_max_true  (\lambda p:nat.eqb (mod n (nth_prime p)) O) n.
-cut ex nat (\lambda i. nth_prime i = smallest_factor n).
+cut \exists i. nth_prime i = smallest_factor n.
 elim Hcut.
 apply ex_intro nat ? a.
 split.