X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Flibrary%2Fnat%2Ford.ma;h=1ec8f68c5d1ad0c077b677bcd1a83767b70b1cee;hb=2632e0520c373f191b81c3975385d77e71314ca7;hp=e9353ba5b31af9903f2c8270025773c8b2c6e7fe;hpb=bec691ac68b66ca288ac0280871afb6597259446;p=helm.git

diff --git a/matita/library/nat/ord.ma b/matita/library/nat/ord.ma
index e9353ba5b..1ec8f68c5 100644
--- a/matita/library/nat/ord.ma
+++ b/matita/library/nat/ord.ma
@@ -17,6 +17,7 @@ set "baseuri" "cic:/matita/nat/ord".
 include "datatypes/constructors.ma".
 include "nat/exp.ma".
 include "nat/gcd.ma".
+include "nat/relevant_equations.ma". (* required by auto paramod *)
 
 (* this definition of log is based on pairs, with a remainder *)