X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Flibrary%2FZ%2Ftimes.ma;fp=helm%2Fmatita%2Flibrary%2FZ%2Ftimes.ma;h=e5e1cdb452fa38ce33a8ba73f95b6ca4a5d5f27d;hb=400b07e007cfbb0b4ce5ed77cfc50f227c491310;hp=27266bf393c41e5457f5cd6723bb8276035df5c6;hpb=5538a4548601ba1c1647ec9dc0fbbd875e5a93fd;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.