]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/matita/library/Z/plus.ma
.ma inclusions corrected/minimized
[helm.git] / helm / matita / library / Z / plus.ma
index 56b960403b7f00e2a9e3e5b4158742a9288ec179..dc743e60bc77f384ecdadd927cee18d5ae085461 100644 (file)
@@ -15,7 +15,6 @@
 set "baseuri" "cic:/matita/Z/plus".
 
 include "Z/z.ma".
-include "nat/compare.ma".
 include "nat/minus.ma".
 
 definition Zplus :Z \to Z \to Z \def