X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Flibrary%2FZ%2Fplus.ma;h=0456ca0b31533f5aed0ccc9fd7561d67b2b3b2bd;hb=73e63e535940a068e660d3688a3c8ebfa1930561;hp=b89f291fbb918684cb595dbd54b5d423259e7e23;hpb=b8c6dd0220fba9ebed2d51d5808790b5949177ea;p=helm.git

diff --git a/helm/matita/library/Z/plus.ma b/helm/matita/library/Z/plus.ma
index b89f291fb..0456ca0b3 100644
--- a/helm/matita/library/Z/plus.ma
+++ b/helm/matita/library/Z/plus.ma
@@ -169,10 +169,10 @@ elim H.reflexivity.
 qed.
 
 theorem Zplus_Zsucc_neg_neg : 
-\forall n,m. (Zsucc (neg n))+(neg m) = Zsucc ((neg n)+(neg m)).
+\forall n,m. Zsucc (neg n) + neg m = Zsucc (neg n + neg m).
 intros.
 apply nat_elim2
-(\lambda n,m. ((Zsucc (neg n))+(neg m)) = Zsucc ((neg n)+(neg m))).intro.
+(\lambda n,m. Zsucc (neg n) + neg m = Zsucc (neg n + neg m)).intro.
 intros.elim n1.
 simplify. reflexivity.
 elim n2.simplify. reflexivity.
@@ -189,7 +189,7 @@ theorem Zplus_Zsucc_neg_pos:
 \forall n,m. Zsucc (neg n)+(pos m) = Zsucc ((neg n)+(pos m)).
 intros.
 apply nat_elim2
-(\lambda n,m. (Zsucc (neg n))+(pos m) = Zsucc ((neg n)+(pos m))).
+(\lambda n,m. Zsucc (neg n) + (pos m) = Zsucc (neg n + pos m)).
 intros.elim n1.
 simplify. reflexivity.
 elim n2.simplify. reflexivity.