]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/matita/library/nat/div_and_mod.ma
.ma inclusions corrected/minimized
[helm.git] / helm / matita / library / nat / div_and_mod.ma
index 73f90e55371c3440aad9bd8e51a116f4bd1b7b7c..ede15596aad479399b646b5f3e78ad9b423cc2fb 100644 (file)
@@ -15,8 +15,6 @@
 set "baseuri" "cic:/matita/nat/div_and_mod".
 
 include "nat/minus.ma".
-include "nat/le_arith.ma".
-include "nat/compare.ma".
 
 let rec mod_aux p m n: nat \def
 match (leb m n) with