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=72e8177b8a559e26be039f624bf1797f0c04fc3c;hb=78044035b4419e569df0d7f6a7f96fa32d21a19d;hp=688957e57396cecb7fd0143c60f171640024b743;hpb=cf8ecd9f8168bcd1b1b6bdb058a4bfbbb374b696;p=helm.git

diff --git a/helm/matita/library/Z/times.ma b/helm/matita/library/Z/times.ma
index 688957e57..72e8177b8 100644
--- a/helm/matita/library/Z/times.ma
+++ b/helm/matita/library/Z/times.ma
@@ -70,58 +70,60 @@ variant sym_Ztimes : \forall x,y:Z. eq Z (Ztimes x y) (Ztimes y x)
 
 theorem associative_Ztimes: associative Z Ztimes.
 change with \forall x,y,z:Z.eq Z (Ztimes (Ztimes x y) z) (Ztimes x (Ztimes y z)).
-intros.
-elim x.simplify.reflexivity.
-elim y.simplify.reflexivity.
-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.
-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.
-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.
-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.
-apply lt_O_times_S_S.
-apply lt_O_times_S_S.
-elim y.simplify.reflexivity.
-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.
-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.
-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.
-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.
-apply lt_O_times_S_S.
-apply lt_O_times_S_S.
+intros.elim x.
+  simplify.reflexivity. 
+  elim y.
+    simplify.reflexivity.
+    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.
+         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.
+         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.
+         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.
+        apply lt_O_times_S_S.apply lt_O_times_S_S.
+  elim y.
+    simplify.reflexivity.
+    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.
+         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.
+         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.
+         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.
+         apply lt_O_times_S_S.apply lt_O_times_S_S.
 qed.
 
 variant assoc_Ztimes : \forall x,y,z:Z. 
@@ -183,21 +185,22 @@ lemma distributive2_Ztimes_pos_Zplus:
 distributive2 nat Z (\lambda n,z. Ztimes (pos n) z) Zplus.
 change with \forall n,y,z.
 eq Z (Ztimes (pos n) (Zplus y z)) (Zplus (Ztimes (pos n) y) (Ztimes (pos n) z)).  
-intros.
-elim y.reflexivity.
-elim z.reflexivity.
-change with
-eq Z (neg (pred (times (S n) (plus (S n1) (S n2)))))
+intros.elim y.
+  reflexivity.
+  elim z.
+    reflexivity.
+    change with
+    eq Z (pos (pred (times (S n) (plus (S n1) (S n2)))))
+      (pos (pred (plus (times (S n) (S n1))(times (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
+    eq Z (neg (pred (times (S n) (plus (S n1) (S n2)))))
      (neg (pred (plus (times (S n) (S n1))(times (S n) (S n2))))).
-rewrite < distr_times_plus.reflexivity.
-apply Ztimes_Zplus_pos_neg_pos.
-elim z.reflexivity.
-apply Ztimes_Zplus_pos_pos_neg.
-change with
-eq Z (pos (pred (times (S n) (plus (S n1) (S n2)))))
-     (pos (pred (plus (times (S n) (S n1))(times (S n) (S n2))))).
-rewrite < distr_times_plus. 
-reflexivity.
+    rewrite < distr_times_plus.reflexivity.
 qed.
 
 variant distr_Ztimes_Zplus_pos: \forall n,y,z.
@@ -226,10 +229,10 @@ eq Z (Ztimes x (Zplus y z)) (Zplus (Ztimes x y) (Ztimes x z)).
 intros.elim x.
 (* case x = OZ *)
 simplify.reflexivity.
-(* case x = neg n *)
-apply distr_Ztimes_Zplus_neg.
 (* case x = pos n *)
 apply distr_Ztimes_Zplus_pos.
+(* case x = neg n *)
+apply distr_Ztimes_Zplus_neg.
 qed.
 
 variant distr_Ztimes_Zplus: \forall x,y,z.