Some lemmas moves to the file they belong to.

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

diff --git a/matita/library/nat/ord.ma b/matita/library/nat/ord.ma
index 5895b3bcddbebcf22f5388cd8b4483027d137012..340e33a865fb809d8beb35e632f4e129fa2bd0dc 100644 (file)
--- a/matita/library/nat/ord.ma
+++ b/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.