More notation here and there.

[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 b89f291fbb918684cb595dbd54b5d423259e7e23..0456ca0b31533f5aed0ccc9fd7561d67b2b3b2bd 100644 (file)
--- 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.