X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Flibrary%2FZ%2Ftimes.ma;h=e5e1cdb452fa38ce33a8ba73f95b6ca4a5d5f27d;hb=97c2d258a5c524eb5c4b85208899d80751a2c82f;hp=27266bf393c41e5457f5cd6723bb8276035df5c6;hpb=10191b6a5e928b355cd1244b7dd15533ebf52924;p=helm.git

diff --git a/helm/matita/library/Z/times.ma b/helm/matita/library/Z/times.ma
index 27266bf39..e5e1cdb45 100644
--- a/helm/matita/library/Z/times.ma
+++ b/helm/matita/library/Z/times.ma
@@ -140,7 +140,7 @@ reflexivity.
 (* we now close all positivity conditions *)
 apply lt_O_times_S_S.                    
 apply lt_O_times_S_S.
-simplify.
+simplify.unfold lt.
 apply le_SO_minus.  exact H.
 qed.