X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Flibrary%2FZ%2Forders.ma;h=c39f693085398eedf4a95a9f15898f05e6cee264;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=186533ea08fb45ae82fd590c8e52f7ffded634c4;hpb=fb94e5a71be508516514dfe50528ccfb3cd2da91;p=helm.git

diff --git a/helm/matita/library/Z/orders.ma b/helm/matita/library/Z/orders.ma
index 186533ea0..c39f69308 100644
--- a/helm/matita/library/Z/orders.ma
+++ b/helm/matita/library/Z/orders.ma
@@ -71,9 +71,9 @@ theorem irreflexive_Zlt: irreflexive Z Zlt.
 change with (\forall x:Z. x < x \to False).
 intro.elim x.exact H.
 cut (neg n < neg n \to False).
-apply Hcut.apply H.simplify.apply not_le_Sn_n.
+apply Hcut.apply H.simplify.unfold lt.apply not_le_Sn_n.
 cut (pos n < pos n \to False).
-apply Hcut.apply H.simplify.apply not_le_Sn_n.
+apply Hcut.apply H.simplify.unfold lt.apply not_le_Sn_n.
 qed.
 
 theorem irrefl_Zlt: irreflexive Z Zlt