X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Flibrary_auto%2Fauto%2FZ%2Ftimes.ma;h=49e8a199e7bb077eb1e1129f5c79a5313d326f5f;hb=562e9adf40098e11d8f0bc2711a7f665360c2231;hp=a95dc4e27df3c2467bb76990f2c487ffa02744f3;hpb=1b839e0367f89503398442b7990fb6b6d1fa2152;p=helm.git

diff --git a/matita/library_auto/auto/Z/times.ma b/matita/library_auto/auto/Z/times.ma
index a95dc4e27..49e8a199e 100644
--- a/matita/library_auto/auto/Z/times.ma
+++ b/matita/library_auto/auto/Z/times.ma
@@ -233,7 +233,7 @@ rewrite < S_pred
   | apply lt_O_times_S_S                    
   | apply lt_O_times_S_S
   ]
-| auto
+| unfold lt.auto
   (*simplify.
   unfold lt.
   apply le_SO_minus.