Much ado about nothing:

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

diff --git a/matita/library/nat/factorization.ma b/matita/library/nat/factorization.ma
index 37a7045924540be5f718043bc79eba2c3c742842..826a2670a70a6c80822c2baeb4764962822af120 100644 (file)
--- 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.