added a function to reorder the metasenv.

[helm.git] / helm / matita / library / Z / times.ma

diff --git a/helm/matita/library/Z/times.ma b/helm/matita/library/Z/times.ma
index 688957e57396cecb7fd0143c60f171640024b743..72e8177b8a559e26be039f624bf1797f0c04fc3c 100644 (file)
--- 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)).
 
 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. 
 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)).  
 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))))).
      (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.
 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.
 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 = 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.
 qed.
 
 variant distr_Ztimes_Zplus: \forall x,y,z.