X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Flibrary%2FZ%2Ftimes.ma;h=e5e1cdb452fa38ce33a8ba73f95b6ca4a5d5f27d;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=19158e300bec21656616171ff60a1052c4007ec7;hpb=fb94e5a71be508516514dfe50528ccfb3cd2da91;p=helm.git

diff --git a/helm/matita/library/Z/times.ma b/helm/matita/library/Z/times.ma
index 19158e300..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.
 
@@ -148,8 +148,8 @@ lemma Ztimes_Zplus_pos_neg_pos: \forall n,p,q:nat.
 (pos n)*((neg p)+(pos q)) = (pos n)*(neg p)+ (pos n)*(pos q). 
 intros.
 simplify. 
-change in match p + n * (S p) with (pred ((S n) * (S p))).
-change in match q + n * (S q) with (pred ((S n) * (S q))).
+change in match (p + n * (S p)) with (pred ((S n) * (S p))).
+change in match (q + n * (S q)) with (pred ((S n) * (S q))).
 rewrite < nat_compare_pred_pred.
 rewrite < nat_compare_times_l.
 rewrite < nat_compare_S_S.