X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fnat%2Ford.ma;h=b7d02f87f3959afdcf85a584e1b2d738983ceb3f;hb=a3eabd0f0dc4de2800c96e29b85ca9a4c06cce0c;hp=1ec8f68c5d1ad0c077b677bcd1a83767b70b1cee;hpb=589ea43c8916e765e43f27b80a2596010527042c;p=helm.git

diff --git a/helm/software/matita/library/nat/ord.ma b/helm/software/matita/library/nat/ord.ma
index 1ec8f68c5..b7d02f87f 100644
--- a/helm/software/matita/library/nat/ord.ma
+++ b/helm/software/matita/library/nat/ord.ma
@@ -168,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.
@@ -213,8 +213,8 @@ unfold.intro.
 elim (divides_times_to_divides ? ? ? H H9).
 apply (absurd ? ? H10 H5).
 apply (absurd ? ? H10 H7).
-rewrite > H6.
-rewrite > H8.
+(* rewrite > H6.
+rewrite > H8. *)
 auto paramodulation.
 unfold prime in H. elim H. assumption.
 qed.