added a function to reorder the metasenv.

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

diff --git a/helm/matita/library/Z/plus.ma b/helm/matita/library/Z/plus.ma
index d2e6ec2b0d2dbe7357814a810d649761b44a4194..56b960403b7f00e2a9e3e5b4158742a9288ec179 100644 (file)
--- a/helm/matita/library/Z/plus.ma
+++ b/helm/matita/library/Z/plus.ma
@@ -73,18 +73,20 @@ qed.
 
 theorem Zpred_Zplus_neg_O : \forall z:Z. Zpred z = (neg O)+z.
 intros.elim z.
-simplify.reflexivity.
-simplify.reflexivity.
-elim n.simplify.reflexivity.
-simplify.reflexivity.
+  simplify.reflexivity.
+  elim n.
+    simplify.reflexivity.
+    simplify.reflexivity.
+  simplify.reflexivity.
 qed.
 
 theorem Zsucc_Zplus_pos_O : \forall z:Z. Zsucc z = (pos O)+z.
 intros.elim z.
-simplify.reflexivity.
-elim n.simplify.reflexivity.
-simplify.reflexivity.
-simplify.reflexivity.
+  simplify.reflexivity.
+  simplify.reflexivity.
+  elim n.
+    simplify.reflexivity.
+    simplify.reflexivity.
 qed.
 
 theorem Zplus_pos_pos:
@@ -129,21 +131,20 @@ qed.
 
 theorem Zplus_Zsucc_Zpred:
 \forall x,y. x+y = (Zsucc x)+(Zpred y).
-intros.
-elim x. elim y.
-simplify.reflexivity.
-simplify.reflexivity.
-rewrite < Zsucc_Zplus_pos_O.
-rewrite > Zsucc_Zpred.reflexivity.
-elim y.rewrite < sym_Zplus.rewrite < sym_Zplus (Zpred OZ).
-rewrite < Zpred_Zplus_neg_O.
-rewrite > Zpred_Zsucc.
-simplify.reflexivity.
-rewrite < Zplus_neg_neg.reflexivity.
-apply Zplus_neg_pos.
-elim y.simplify.reflexivity.
-apply Zplus_pos_neg.
-apply Zplus_pos_pos.
+intros.elim x. 
+  elim y.
+    simplify.reflexivity.
+    rewrite < Zsucc_Zplus_pos_O.rewrite > Zsucc_Zpred.reflexivity.
+    simplify.reflexivity.
+  elim y.
+    simplify.reflexivity.
+    apply Zplus_pos_pos.
+    apply Zplus_pos_neg.
+  elim y.
+    rewrite < sym_Zplus.rewrite < sym_Zplus (Zpred OZ).
+     rewrite < Zpred_Zplus_neg_O.rewrite > Zpred_Zsucc.simplify.reflexivity.
+    apply Zplus_neg_pos.
+    rewrite < Zplus_neg_neg.reflexivity.
 qed.
 
 theorem Zplus_Zsucc_pos_pos : 
@@ -204,17 +205,19 @@ reflexivity.
 qed.
 
 theorem Zplus_Zsucc : \forall x,y:Z. (Zsucc x)+y = Zsucc (x+y).
-intros.elim x.elim y.
-simplify. reflexivity.
-rewrite < Zsucc_Zplus_pos_O.reflexivity.
-simplify.reflexivity.
-elim y.rewrite < sym_Zplus.rewrite < sym_Zplus OZ.simplify.reflexivity.
-apply Zplus_Zsucc_neg_neg.
-apply Zplus_Zsucc_neg_pos.
-elim y.
-rewrite < sym_Zplus OZ.reflexivity.
-apply Zplus_Zsucc_pos_neg.
-apply Zplus_Zsucc_pos_pos.
+intros.elim x.
+  elim y.
+    simplify. reflexivity.
+    simplify.reflexivity.
+    rewrite < Zsucc_Zplus_pos_O.reflexivity.
+  elim y.
+    rewrite < sym_Zplus OZ.reflexivity.
+    apply Zplus_Zsucc_pos_pos.
+    apply Zplus_Zsucc_pos_neg.
+  elim y.
+    rewrite < sym_Zplus.rewrite < sym_Zplus OZ.simplify.reflexivity.
+    apply Zplus_Zsucc_neg_pos.
+    apply Zplus_Zsucc_neg_neg.
 qed.
 
 theorem Zplus_Zpred: \forall x,y:Z. (Zpred x)+y = Zpred (x+y).
@@ -232,23 +235,18 @@ qed.
 theorem associative_Zplus: associative Z Zplus.
 change with \forall x,y,z:Z. (x + y) + z = x + (y + z). 
 (* simplify. *)
-intros.elim x.simplify.reflexivity.
-elim n.rewrite < (Zpred_Zplus_neg_O (y+z)).
-rewrite < (Zpred_Zplus_neg_O y).
-rewrite < Zplus_Zpred.
-reflexivity.
-rewrite > Zplus_Zpred (neg n1).
-rewrite > Zplus_Zpred (neg n1).
-rewrite > Zplus_Zpred ((neg n1)+y).
-apply eq_f.assumption.
-elim n.rewrite < Zsucc_Zplus_pos_O.
-rewrite < Zsucc_Zplus_pos_O.
-rewrite > Zplus_Zsucc.
-reflexivity.
-rewrite > Zplus_Zsucc (pos n1).
-rewrite > Zplus_Zsucc (pos n1).
-rewrite > Zplus_Zsucc ((pos n1)+y).
-apply eq_f.assumption.
+intros.elim x.
+  simplify.reflexivity.
+  elim n.
+    rewrite < Zsucc_Zplus_pos_O.rewrite < Zsucc_Zplus_pos_O.
+     rewrite > Zplus_Zsucc.reflexivity.
+    rewrite > Zplus_Zsucc (pos n1).rewrite > Zplus_Zsucc (pos n1).
+     rewrite > Zplus_Zsucc ((pos n1)+y).apply eq_f.assumption.
+  elim n.
+    rewrite < (Zpred_Zplus_neg_O (y+z)).rewrite < (Zpred_Zplus_neg_O y).
+     rewrite < Zplus_Zpred.reflexivity.
+    rewrite > Zplus_Zpred (neg n1).rewrite > Zplus_Zpred (neg n1).
+     rewrite > Zplus_Zpred ((neg n1)+y).apply eq_f.assumption.
 qed.
 
 variant assoc_Zplus : \forall x,y,z:Z.  (x+y)+z = x+(y+z)