library = yes!

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

diff --git a/matita/library/nat/ord.ma b/matita/library/nat/ord.ma
index e9353ba5b31af9903f2c8270025773c8b2c6e7fe..ba08a0dcf5ba21536cb4830f10c22e88b5eac00a 100644 (file)
--- 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 *)
 
@@ -167,7 +168,7 @@ apply p_ord_exp
   apply le_times_l.
   assumption.
   apply le_times_r.assumption.
-  alias id "not_eq_to_le_to_lt" = "cic:/matita/algebra/finite_groups/not_eq_to_le_to_lt.con".
+alias id "not_eq_to_le_to_lt" = "cic:/matita/algebra/finite_groups/not_eq_to_le_to_lt.con".
 apply not_eq_to_le_to_lt.
   unfold.intro.apply H1.
   rewrite < H3.
@@ -212,9 +213,9 @@ unfold.intro.
 elim (divides_times_to_divides ? ? ? H H9).
 apply (absurd ? ? H10 H5).
 apply (absurd ? ? H10 H7).
-rewrite > H6.
-rewrite > H8.
-auto paramodulation.
+(* rewrite > H6.
+rewrite > H8. *)
+auto paramodulation library=yes.
 unfold prime in H. elim H. assumption.
 qed.