X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Flibrary%2FZ%2Fplus.ma;h=2b439b92e273c83d0e9175bd402d32d0fb363b64;hb=41af0583fbc8183183d389303951dca94f2965b0;hp=976f6cfb3ce01d379244fc66ec964a99563917d3;hpb=7f2444c2670cadafddd8785b687ef312158376b0;p=helm.git

diff --git a/matita/library/Z/plus.ma b/matita/library/Z/plus.ma
index 976f6cfb3..2b439b92e 100644
--- a/matita/library/Z/plus.ma
+++ b/matita/library/Z/plus.ma
@@ -299,3 +299,7 @@ rewrite > nat_compare_n_n.
 simplify.apply refl_eq.
 qed.
 
+(* minus *)
+definition Zminus : Z \to Z \to Z \def \lambda x,y:Z. x + (-y).
+
+interpretation "integer minus" 'minus x y = (cic:/matita/Z/plus/Zminus.con x y).