X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Flibrary%2Fnat%2Ford.ma;h=24874c08af2fd10d2e3286f01e388940f3390d51;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=b982accb37727b46841bbc7a8fc3e8a11dd31865;hpb=fb94e5a71be508516514dfe50528ccfb3cd2da91;p=helm.git

diff --git a/helm/matita/library/nat/ord.ma b/helm/matita/library/nat/ord.ma
index b982accb3..24874c08a 100644
--- a/helm/matita/library/nat/ord.ma
+++ b/helm/matita/library/nat/ord.ma
@@ -167,7 +167,7 @@ generalize in match (H (n1 / m) m).
 elim (p_ord_aux n (n1 / m) m).
 apply H5.assumption.
 apply eq_mod_O_to_lt_O_div.
-apply (trans_lt ? (S O)).simplify.apply le_n.
+apply (trans_lt ? (S O)).unfold lt.apply le_n.
 assumption.assumption.assumption.
 apply le_S_S_to_le.
 apply (trans_le ? n1).change with (n1 / m < n1).
@@ -175,9 +175,7 @@ apply lt_div_n_m_n.assumption.assumption.assumption.
 intros.
 change with (n1 \mod m \neq O).
 rewrite > H4.
-(* Andrea: META NOT FOUND !!!  
-rewrite > sym_eq. *)
-simplify.intro.
+unfold Not.intro.
 apply (not_eq_O_S m1).
 rewrite > H5.reflexivity.
 qed.