More notation.

diff --git a/helm/matita/library/Z/z.ma b/helm/matita/library/Z/z.ma
index 118cdd55eaaa3eb8e0f6b5eb35e1461d12dd8e1b..d3bc2ee2584529c00802746e4e5e792ea0c4242e 100644 (file)
--- a/helm/matita/library/Z/z.ma
+++ b/helm/matita/library/Z/z.ma
@@ -108,21 +108,21 @@ definition Zplus :Z \to Z \to Z \def
     | (pos m) \Rightarrow
         match y with
          [ OZ \Rightarrow x
-         | (pos n) \Rightarrow (pos (S (plus m n)))
+         | (pos n) \Rightarrow (pos (S (m+n)))
          | (neg n) \Rightarrow 
               match nat_compare m n with
-                [ LT \Rightarrow (neg (pred (minus n m)))
+                [ LT \Rightarrow (neg (pred (n-m)))
                 | EQ \Rightarrow OZ
-                | GT \Rightarrow (pos (pred (minus m n)))]]
+                | GT \Rightarrow (pos (pred (m-n)))]]
     | (neg m) \Rightarrow
         match y with
          [ OZ \Rightarrow x
          | (pos n) \Rightarrow 
               match nat_compare m n with
-                [ LT \Rightarrow (pos (pred (minus n m)))
+                [ LT \Rightarrow (pos (pred (n-m)))
                 | EQ \Rightarrow OZ
-                | GT \Rightarrow (neg (pred (minus m n)))]     
-         | (neg n) \Rightarrow (neg (S (plus m n)))]].
+                | GT \Rightarrow (neg (pred (m-n)))]     
+         | (neg n) \Rightarrow (neg (S (m+n)))]].
 
 (*CSC: the URI must disappear: there is a bug now *)
 interpretation "integer plus" 'plus x y = (cic:/matita/Z/z/Zplus.con x y).