X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Flibrary%2Fnat%2Ffactorization.ma;h=826a2670a70a6c80822c2baeb4764962822af120;hb=cd91767a396b7bbc72e6e3ee90a3b758421f935d;hp=37a7045924540be5f718043bc79eba2c3c742842;hpb=324d594e5e37081d945d631986447a95a1937634;p=helm.git

diff --git a/matita/library/nat/factorization.ma b/matita/library/nat/factorization.ma
index 37a704592..826a2670a 100644
--- a/matita/library/nat/factorization.ma
+++ b/matita/library/nat/factorization.ma
@@ -399,7 +399,6 @@ apply (not_eq_O_S (S m1)).
 rewrite > Hcut.rewrite < H1.rewrite < times_n_O.reflexivity.
 apply le_to_or_lt_eq.apply le_O_n.
 (* prova del cut *)
-goal 20.
 apply (p_ord_aux_to_exp (S(S m1))).
 apply lt_O_nth_prime_n.
 assumption.