.ma inclusions corrected/minimized

[helm.git] / helm / matita / library / nat / le_arith.ma

diff --git a/helm/matita/library/nat/le_arith.ma b/helm/matita/library/nat/le_arith.ma
index a36f96bd451caba6a4091f0e7ecd9ea530957ed1..dbf7b1c4298ca340b14791da95e44f1bfab3e988 100644 (file)
--- 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: