]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/matita/library/nat/plus.ma
Added a new contrib div_and_mod and few modifs here and there.
[helm.git] / helm / matita / library / nat / plus.ma
index fbb3fcc90b76e4ceb7b037336f3393336ccffea3..e8750d0cba0f41a0995a23524a8d6f887a83204e 100644 (file)
@@ -14,7 +14,6 @@
 
 set "baseuri" "cic:/matita/nat/plus".
 
-include "logic/equality.ma".
 include "nat/nat.ma".
 
 let rec plus n m \def