X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Flibrary%2FZ%2Fz.ma;h=5aa5d90832a7359dc9da1d20d6581c1e1a3b7a21;hb=1bcad789810fd37d346e690f18557aeedc6fe08c;hp=afe80e736030489184d85257a693ecb08316e466;hpb=9c8bb7e7c2548d2f37e5387cdce45df2b8fc9b43;p=helm.git

diff --git a/helm/matita/library/Z/z.ma b/helm/matita/library/Z/z.ma
index afe80e736..5aa5d9083 100644
--- a/helm/matita/library/Z/z.ma
+++ b/helm/matita/library/Z/z.ma
@@ -56,13 +56,13 @@ match OZ_test z with
 intros.elim z.
 simplify.reflexivity.
 simplify.intros.
-cut match neg e1 with 
+cut match neg n with 
 [ OZ \Rightarrow True 
 | (pos n) \Rightarrow False
 | (neg n) \Rightarrow False].
 apply Hcut.rewrite > H.simplify.exact I.
 simplify.intros.
-cut match pos e2 with 
+cut match pos n with 
 [ OZ \Rightarrow True 
 | (pos n) \Rightarrow False
 | (neg n) \Rightarrow False].
@@ -89,7 +89,7 @@ definition Zpred \def
 
 theorem Zpred_Zsucc: \forall z:Z. eq Z (Zpred (Zsucc z)) z.
 intros.elim z.reflexivity.
-elim e1.reflexivity.
+elim n.reflexivity.
 reflexivity.
 reflexivity.
 qed.
@@ -97,7 +97,7 @@ qed.
 theorem Zsucc_Zpred: \forall z:Z. eq Z (Zsucc (Zpred z)) z.
 intros.elim z.reflexivity.
 reflexivity.
-elim e2.reflexivity.
+elim n.reflexivity.
 reflexivity.
 qed.
 
@@ -155,14 +155,14 @@ theorem Zpred_Zplus_neg_O : \forall z:Z. eq Z (Zpred z) (Zplus (neg O) z).
 intros.elim z.
 simplify.reflexivity.
 simplify.reflexivity.
-elim e2.simplify.reflexivity.
+elim n.simplify.reflexivity.
 simplify.reflexivity.
 qed.
 
 theorem Zsucc_Zplus_pos_O : \forall z:Z. eq Z (Zsucc z) (Zplus (pos O) z).
 intros.elim z.
 simplify.reflexivity.
-elim e1.simplify.reflexivity.
+elim n.simplify.reflexivity.
 simplify.reflexivity.
 simplify.reflexivity.
 qed.
@@ -238,7 +238,7 @@ apply nat_elim2
 (\lambda n,m. eq Z (Zplus (Zsucc (pos n)) (neg m)) (Zsucc (Zplus (pos n) (neg m)))).intro.
 intros.elim n1.
 simplify. reflexivity.
-elim e1.simplify. reflexivity.
+elim n2.simplify. reflexivity.
 simplify. reflexivity.
 intros. elim n1.
 simplify. reflexivity.
@@ -255,7 +255,7 @@ apply nat_elim2
 (\lambda n,m. eq Z (Zplus (Zsucc (neg n)) (neg m)) (Zsucc (Zplus (neg n) (neg m)))).intro.
 intros.elim n1.
 simplify. reflexivity.
-elim e1.simplify. reflexivity.
+elim n2.simplify. reflexivity.
 simplify. reflexivity.
 intros. elim n1.
 simplify. reflexivity.
@@ -272,7 +272,7 @@ apply nat_elim2
 (\lambda n,m. eq Z (Zplus (Zsucc (neg n)) (pos m)) (Zsucc (Zplus (neg n) (pos m)))).
 intros.elim n1.
 simplify. reflexivity.
-elim e1.simplify. reflexivity.
+elim n2.simplify. reflexivity.
 simplify. reflexivity.
 intros. elim n1.
 simplify. reflexivity.
@@ -313,21 +313,21 @@ theorem associative_Zplus: associative Z Zplus.
 change with \forall x,y,z:Z. eq Z (Zplus (Zplus x y) z) (Zplus x (Zplus y z)). 
 (* simplify. *)
 intros.elim x.simplify.reflexivity.
-elim e1.rewrite < (Zpred_Zplus_neg_O (Zplus y z)).
+elim n.rewrite < (Zpred_Zplus_neg_O (Zplus y z)).
 rewrite < (Zpred_Zplus_neg_O y).
 rewrite < Zplus_Zpred.
 reflexivity.
-rewrite > Zplus_Zpred (neg e).
-rewrite > Zplus_Zpred (neg e).
-rewrite > Zplus_Zpred (Zplus (neg e) y).
+rewrite > Zplus_Zpred (neg n1).
+rewrite > Zplus_Zpred (neg n1).
+rewrite > Zplus_Zpred (Zplus (neg n1) y).
 apply eq_f.assumption.
-elim e2.rewrite < Zsucc_Zplus_pos_O.
+elim n.rewrite < Zsucc_Zplus_pos_O.
 rewrite < Zsucc_Zplus_pos_O.
 rewrite > Zplus_Zsucc.
 reflexivity.
-rewrite > Zplus_Zsucc (pos e1).
-rewrite > Zplus_Zsucc (pos e1).
-rewrite > Zplus_Zsucc (Zplus (pos e1) y).
+rewrite > Zplus_Zsucc (pos n1).
+rewrite > Zplus_Zsucc (pos n1).
+rewrite > Zplus_Zsucc (Zplus (pos n1) y).
 apply eq_f.assumption.
 qed.