X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Flibrary%2Fnat%2Fle_arith.ma;h=dbf7b1c4298ca340b14791da95e44f1bfab3e988;hb=2ecd65dbcc1388bb2dfe6425e6ef1b2e3f45c4ac;hp=a36f96bd451caba6a4091f0e7ecd9ea530957ed1;hpb=7bbce6bc163892cfd99cfcda65db42001b86789f;p=helm.git

diff --git a/helm/matita/library/nat/le_arith.ma b/helm/matita/library/nat/le_arith.ma
index a36f96bd4..dbf7b1c42 100644
--- a/helm/matita/library/nat/le_arith.ma
+++ b/helm/matita/library/nat/le_arith.ma
@@ -14,10 +14,8 @@
 
 set "baseuri" "cic:/matita/nat/le_arith".
 
-include "higher_order_defs/functions.ma".
 include "nat/times.ma".
 include "nat/orders.ma".
-include "nat/compare.ma".
 
 (* plus *)
 theorem monotonic_le_plus_r: