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

diff --git a/helm/matita/library/Z/times.ma b/helm/matita/library/Z/times.ma
index e356c4357..e5e1cdb45 100644
--- a/helm/matita/library/Z/times.ma
+++ b/helm/matita/library/Z/times.ma
@@ -50,17 +50,17 @@ simplify.reflexivity.
 simplify.reflexivity.
 qed.
 theorem symmetric_Ztimes : symmetric Z Ztimes.
-change with \forall x,y:Z. x*y = y*x.
+change with (\forall x,y:Z. x*y = y*x).
 intros.elim x.rewrite > Ztimes_z_OZ.reflexivity.
 elim y.simplify.reflexivity. 
-change with pos (pred ((S n) * (S n1))) = pos (pred ((S n1) * (S n))).
+change with (pos (pred ((S n) * (S n1))) = pos (pred ((S n1) * (S n)))).
 rewrite < sym_times.reflexivity.
-change with neg (pred ((S n) * (S n1))) = neg (pred ((S n1) * (S n))).
+change with (neg (pred ((S n) * (S n1))) = neg (pred ((S n1) * (S n)))).
 rewrite < sym_times.reflexivity.
 elim y.simplify.reflexivity.
-change with neg (pred ((S n) * (S n1))) = neg (pred ((S n1) * (S n))).
+change with (neg (pred ((S n) * (S n1))) = neg (pred ((S n1) * (S n)))).
 rewrite < sym_times.reflexivity.
-change with pos (pred ((S n) * (S n1))) = pos (pred ((S n1) * (S n))).
+change with (pos (pred ((S n) * (S n1))) = pos (pred ((S n1) * (S n)))).
 rewrite < sym_times.reflexivity.
 qed.
 
@@ -68,7 +68,7 @@ variant sym_Ztimes : \forall x,y:Z. x*y = y*x
 \def symmetric_Ztimes.
 
 theorem associative_Ztimes: associative Z Ztimes.
-change with \forall x,y,z:Z. (x*y)*z = x*(y*z).
+change with (\forall x,y,z:Z. (x*y)*z = x*(y*z)).
 intros.elim x.
   simplify.reflexivity. 
   elim y.
@@ -76,25 +76,25 @@ intros.elim x.
     elim z.
       simplify.reflexivity.
       change with 
-       pos (pred ((S (pred ((S n) * (S n1)))) * (S n2))) =
-       pos (pred ((S n) * (S (pred ((S n1) * (S n2)))))).
+       (pos (pred ((S (pred ((S n) * (S n1)))) * (S n2))) =
+       pos (pred ((S n) * (S (pred ((S n1) * (S n2))))))).
         rewrite < S_pred.rewrite < S_pred.rewrite < assoc_times.reflexivity.
          apply lt_O_times_S_S.apply lt_O_times_S_S.
       change with 
-       neg (pred ((S (pred ((S n) * (S n1)))) * (S n2))) =
-       neg (pred ((S n) * (S (pred ((S n1) * (S n2)))))).
+       (neg (pred ((S (pred ((S n) * (S n1)))) * (S n2))) =
+       neg (pred ((S n) * (S (pred ((S n1) * (S n2))))))).
         rewrite < S_pred.rewrite < S_pred.rewrite < assoc_times.reflexivity.
          apply lt_O_times_S_S.apply lt_O_times_S_S.
     elim z.
       simplify.reflexivity.
       change with 
-       neg (pred ((S (pred ((S n) * (S n1)))) * (S n2))) =
-       neg (pred ((S n) * (S (pred ((S n1) * (S n2)))))).
+       (neg (pred ((S (pred ((S n) * (S n1)))) * (S n2))) =
+       neg (pred ((S n) * (S (pred ((S n1) * (S n2))))))).
         rewrite < S_pred.rewrite < S_pred.rewrite < assoc_times.reflexivity.
          apply lt_O_times_S_S.apply lt_O_times_S_S.
       change with 
-       pos (pred ((S (pred ((S n) * (S n1)))) * (S n2))) =
-       pos(pred ((S n) * (S (pred ((S n1) * (S n2)))))).
+       (pos (pred ((S (pred ((S n) * (S n1)))) * (S n2))) =
+       pos(pred ((S n) * (S (pred ((S n1) * (S n2))))))).
         rewrite < S_pred.rewrite < S_pred.rewrite < assoc_times.reflexivity.
         apply lt_O_times_S_S.apply lt_O_times_S_S.
   elim y.
@@ -102,25 +102,25 @@ intros.elim x.
     elim z.
       simplify.reflexivity.
       change with 
-       neg (pred ((S (pred ((S n) * (S n1)))) * (S n2))) =
-       neg (pred ((S n) * (S (pred ((S n1) * (S n2)))))).
+       (neg (pred ((S (pred ((S n) * (S n1)))) * (S n2))) =
+       neg (pred ((S n) * (S (pred ((S n1) * (S n2))))))).
         rewrite < S_pred.rewrite < S_pred.rewrite < assoc_times.reflexivity.
          apply lt_O_times_S_S.apply lt_O_times_S_S.
       change with 
-       pos (pred ((S (pred ((S n) * (S n1)))) * (S n2))) =
-       pos (pred ((S n) * (S (pred ((S n1) * (S n2)))))).
+       (pos (pred ((S (pred ((S n) * (S n1)))) * (S n2))) =
+       pos (pred ((S n) * (S (pred ((S n1) * (S n2))))))).
         rewrite < S_pred.rewrite < S_pred.rewrite < assoc_times.reflexivity.
          apply lt_O_times_S_S.apply lt_O_times_S_S.
     elim z.
       simplify.reflexivity.
       change with 
-       pos (pred ((S (pred ((S n) * (S n1)))) * (S n2))) =
-       pos (pred ((S n) * (S (pred ((S n1) * (S n2)))))).
+       (pos (pred ((S (pred ((S n) * (S n1)))) * (S n2))) =
+       pos (pred ((S n) * (S (pred ((S n1) * (S n2))))))).
         rewrite < S_pred.rewrite < S_pred.rewrite < assoc_times.reflexivity.
          apply lt_O_times_S_S.apply lt_O_times_S_S.
       change with 
-       neg (pred ((S (pred ((S n) * (S n1)))) * (S n2))) =
-       neg(pred ((S n) * (S (pred ((S n1) * (S n2)))))).
+       (neg (pred ((S (pred ((S n) * (S n1)))) * (S n2))) =
+       neg(pred ((S n) * (S (pred ((S n1) * (S n2))))))).
         rewrite < S_pred.rewrite < S_pred.rewrite < assoc_times.reflexivity.
          apply lt_O_times_S_S.apply lt_O_times_S_S.
 qed.
@@ -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,22 +148,22 @@ 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.
-apply nat_compare_elim p q.
+apply (nat_compare_elim p q).
 intro.
 (* uff *)
-change with pos (pred ((S n) * (S (pred ((S q) - (S p)))))) =
-            pos (pred ((pred ((S n) * (S q))) - (pred ((S n) * (S p))))).
-rewrite < times_minus1 n q p H.reflexivity.
+change with (pos (pred ((S n) * (S (pred ((S q) - (S p)))))) =
+            pos (pred ((pred ((S n) * (S q))) - (pred ((S n) * (S p)))))).
+rewrite < (times_minus1 n q p H).reflexivity.
 intro.rewrite < H.simplify.reflexivity.
 intro.
-change with neg (pred ((S n) * (S (pred ((S p) - (S q)))))) =
-            neg (pred ((pred ((S n) * (S p))) - (pred ((S n) * (S q))))). 
-rewrite < times_minus1 n p q H.reflexivity.                                 
+change with (neg (pred ((S n) * (S (pred ((S p) - (S q)))))) =
+            neg (pred ((pred ((S n) * (S p))) - (pred ((S n) * (S q)))))). 
+rewrite < (times_minus1 n p q H).reflexivity.                                 
 (* two more positivity conditions from nat_compare_pred_pred *)   
 apply lt_O_times_S_S.  
 apply lt_O_times_S_S. 
@@ -179,23 +179,23 @@ qed.
 
 lemma distributive2_Ztimes_pos_Zplus: 
 distributive2 nat Z (\lambda n,z. (pos n) * z) Zplus.
-change with \forall n,y,z.
-(pos n) * (y + z) = (pos n) * y + (pos n) * z.  
+change with (\forall n,y,z.
+(pos n) * (y + z) = (pos n) * y + (pos n) * z).  
 intros.elim y.
   reflexivity.
   elim z.
     reflexivity.
     change with
-     pos (pred ((S n) * ((S n1) + (S n2)))) =
-     pos (pred ((S n) * (S n1) + (S n) * (S n2))).
+     (pos (pred ((S n) * ((S n1) + (S n2)))) =
+     pos (pred ((S n) * (S n1) + (S n) * (S n2)))).
       rewrite < distr_times_plus.reflexivity.
     apply Ztimes_Zplus_pos_pos_neg.
   elim z.
     reflexivity.
     apply Ztimes_Zplus_pos_neg_pos.
     change with
-     neg (pred ((S n) * ((S n1) + (S n2)))) =
-     neg (pred ((S n) * (S n1) + (S n) * (S n2))).
+     (neg (pred ((S n) * ((S n1) + (S n2)))) =
+     neg (pred ((S n) * (S n1) + (S n) * (S n2)))).
     rewrite < distr_times_plus.reflexivity.
 qed.
 
@@ -205,8 +205,8 @@ distributive2_Ztimes_pos_Zplus.
 
 lemma distributive2_Ztimes_neg_Zplus : 
 distributive2 nat Z (\lambda n,z. (neg n) * z) Zplus.
-change with \forall n,y,z.
-(neg n) * (y + z) = (neg n) * y + (neg n) * z.  
+change with (\forall n,y,z.
+(neg n) * (y + z) = (neg n) * y + (neg n) * z).  
 intros.
 rewrite > Ztimes_neg_Zopp. 
 rewrite > distr_Ztimes_Zplus_pos.
@@ -220,7 +220,7 @@ variant distr_Ztimes_Zplus_neg: \forall n,y,z.
 distributive2_Ztimes_neg_Zplus.
 
 theorem distributive_Ztimes_Zplus: distributive Z Ztimes Zplus.
-change with \forall x,y,z:Z. x * (y + z) = x*y + x*z.
+change with (\forall x,y,z:Z. x * (y + z) = x*y + x*z).
 intros.elim x.
 (* case x = OZ *)
 simplify.reflexivity.