auto rewritten with only one tail recursive function.

[helm.git] / matita / library_auto / auto / Z / times.ma

diff --git a/matita/library_auto/auto/Z/times.ma b/matita/library_auto/auto/Z/times.ma
index a95dc4e27df3c2467bb76990f2c487ffa02744f3..49e8a199e7bb077eb1e1129f5c79a5313d326f5f 100644 (file)
--- 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.