X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Flibrary%2Fnat%2Ffactorization.ma;h=c8127a1fa8cde6467be67ca32b6549466b56a566;hb=2ecd65dbcc1388bb2dfe6425e6ef1b2e3f45c4ac;hp=4628eca13c1d86f1f545f95784b118f814b4832b;hpb=b8c6dd0220fba9ebed2d51d5808790b5949177ea;p=helm.git

diff --git a/helm/matita/library/nat/factorization.ma b/helm/matita/library/nat/factorization.ma
index 4628eca13..c8127a1fa 100644
--- 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.