X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Flibrary%2FZ%2Ftimes.ma;h=a36bd078c01877187072ee6fb804fd44beaacdaa;hb=2ecd65dbcc1388bb2dfe6425e6ef1b2e3f45c4ac;hp=72e8177b8a559e26be039f624bf1797f0c04fc3c;hpb=78044035b4419e569df0d7f6a7f96fa32d21a19d;p=helm.git

diff --git a/helm/matita/library/Z/times.ma b/helm/matita/library/Z/times.ma
index 72e8177b8..a36bd078c 100644
--- a/helm/matita/library/Z/times.ma
+++ b/helm/matita/library/Z/times.ma
@@ -16,7 +16,6 @@ set "baseuri" "cic:/matita/Z/times".
 
 include "nat/lt_arith.ma".
 include "Z/plus.ma".
-include "higher_order_defs/functions.ma".
 
 definition Ztimes :Z \to Z \to Z \def
 \lambda x,y.
@@ -79,24 +78,24 @@ intros.elim x.
       change with 
       eq Z (pos (pred (times (S (pred (times (S n) (S n1)))) (S n2))))
         (pos (pred (times (S n) (S (pred (times (S n1) (S n2))))))).
-        rewrite < S_pred ? ?.rewrite < S_pred ? ?.rewrite < assoc_times.reflexivity.
+        rewrite < S_pred.rewrite < S_pred.rewrite < assoc_times.reflexivity.
          apply lt_O_times_S_S.apply lt_O_times_S_S.
       change with 
       eq Z (neg (pred (times (S (pred (times (S n) (S n1)))) (S n2))))
         (neg (pred (times (S n) (S (pred (times (S n1) (S n2))))))).
-        rewrite < S_pred ? ?.rewrite < S_pred ? ?.rewrite < assoc_times.reflexivity.
+        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 
       eq Z (neg (pred (times (S (pred (times (S n) (S n1)))) (S n2))))
         (neg (pred (times (S n) (S (pred (times (S n1) (S n2))))))).
-        rewrite < S_pred ? ?.rewrite < S_pred ? ?.rewrite < assoc_times.reflexivity.
+        rewrite < S_pred.rewrite < S_pred.rewrite < assoc_times.reflexivity.
          apply lt_O_times_S_S.apply lt_O_times_S_S.
       change with 
       eq Z (pos (pred (times (S (pred (times (S n) (S n1)))) (S n2))))
         (pos(pred (times (S n) (S (pred (times (S n1) (S n2))))))).
-        rewrite < S_pred ? ?.rewrite < S_pred ? ?.rewrite < assoc_times.reflexivity.
+        rewrite < S_pred.rewrite < S_pred.rewrite < assoc_times.reflexivity.
         apply lt_O_times_S_S.apply lt_O_times_S_S.
   elim y.
     simplify.reflexivity.
@@ -105,24 +104,24 @@ intros.elim x.
       change with 
       eq Z (neg (pred (times (S (pred (times (S n) (S n1)))) (S n2))))
         (neg (pred (times (S n) (S (pred (times (S n1) (S n2))))))).
-        rewrite < S_pred ? ?.rewrite < S_pred ? ?.rewrite < assoc_times.reflexivity.
+        rewrite < S_pred.rewrite < S_pred.rewrite < assoc_times.reflexivity.
          apply lt_O_times_S_S.apply lt_O_times_S_S.
       change with 
       eq Z (pos (pred (times (S (pred (times (S n) (S n1)))) (S n2))))
         (pos (pred (times (S n) (S (pred (times (S n1) (S n2))))))).
-        rewrite < S_pred ? ?.rewrite < S_pred ? ?.rewrite < assoc_times.reflexivity.
+        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 
       eq Z (pos (pred (times (S (pred (times (S n) (S n1)))) (S n2))))
         (pos (pred (times (S n) (S (pred (times (S n1) (S n2))))))).
-        rewrite < S_pred ? ?.rewrite < S_pred ? ?.rewrite < assoc_times.reflexivity.
+        rewrite < S_pred.rewrite < S_pred.rewrite < assoc_times.reflexivity.
          apply lt_O_times_S_S.apply lt_O_times_S_S.
       change with 
       eq Z (neg (pred (times (S (pred (times (S n) (S n1)))) (S n2))))
         (neg(pred (times (S n) (S (pred (times (S n1) (S n2))))))).
-        rewrite < S_pred ? ?.rewrite < S_pred ? ?.rewrite < assoc_times.reflexivity.
+        rewrite < S_pred.rewrite < S_pred.rewrite < assoc_times.reflexivity.
          apply lt_O_times_S_S.apply lt_O_times_S_S.
 qed.
 
@@ -135,8 +134,8 @@ eq nat (times (S n) (S (pred (minus (S p) (S q)))))
        (minus (pred (times (S n) (S p))) 
               (pred (times (S n) (S q)))).
 intros.
-rewrite < S_pred ? ?.  
-rewrite > minus_pred_pred ? ? ? ?.
+rewrite < S_pred.  
+rewrite > minus_pred_pred.
 rewrite < distr_times_minus. 
 reflexivity.  
 (* we now close all positivity conditions *)
@@ -152,7 +151,7 @@ intros.
 simplify. 
 change in match (plus p (times n (S p))) with (pred (times (S n) (S p))).
 change in match (plus q (times n (S q))) with (pred (times (S n) (S q))).
-rewrite < nat_compare_pred_pred ? ? ? ?.
+rewrite < nat_compare_pred_pred.
 rewrite < nat_compare_times_l.
 rewrite < nat_compare_S_S.
 apply nat_compare_elim p q.
@@ -237,4 +236,4 @@ qed.
 
 variant distr_Ztimes_Zplus: \forall x,y,z.
 eq Z (Ztimes x (Zplus y z)) (Zplus (Ztimes x y) (Ztimes x z)) \def
-distributive_Ztimes_Zplus.
\ No newline at end of file
+distributive_Ztimes_Zplus.