X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fnat%2Ford.ma;h=340e33a865fb809d8beb35e632f4e129fa2bd0dc;hb=34d2f477be65e3fd26bfb6d43a3dd0807274549b;hp=5895b3bcddbebcf22f5388cd8b4483027d137012;hpb=d8b17e4c77989c669c9db3847bd6b9e7c236e2c3;p=helm.git

diff --git a/helm/software/matita/library/nat/ord.ma b/helm/software/matita/library/nat/ord.ma
index 5895b3bcd..340e33a86 100644
--- a/helm/software/matita/library/nat/ord.ma
+++ b/helm/software/matita/library/nat/ord.ma
@@ -166,8 +166,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".
-apply not_eq_to_le_to_lt.
+  apply not_eq_to_le_to_lt.
   unfold.intro.apply H1.
   rewrite < H3.
   apply (witness ? r r ?).simplify.apply plus_n_O.
@@ -456,4 +455,4 @@ theorem mod_p_ord_inv:
 intros.rewrite > eq_p_ord_inv.
 apply mod_plus_times.
 assumption.
-qed.
\ No newline at end of file
+qed.