auto rewritten with only one tail recursive function.

[helm.git] / matita / library_auto / auto / nat / factorization.ma

diff --git a/matita/library_auto/auto/nat/factorization.ma b/matita/library_auto/auto/nat/factorization.ma
index 073318f9e8a0f9bf3fa6730b664ccc25e2a09461..69acf1837fcc3ab912eea14bdf0ad28248c23593 100644 (file)
--- a/matita/library_auto/auto/nat/factorization.ma
+++ b/matita/library_auto/auto/nat/factorization.ma
@@ -598,7 +598,6 @@ apply (nat_case n)
           ]
         ]
       | (* prova del cut *)
-        goal 20.
         apply (p_ord_aux_to_exp (S(S m1)));auto
         (*[ apply lt_O_nth_prime_n
         | assumption