X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fmatita%2Flibrary%2FZ%2Forders.ma;h=0a3cfbe1f680dccafb3c37f5a9cc73ab8ced8c9c;hb=ebb14e0084aecd167bc42245625c4eb3167df9d5;hp=c39f693085398eedf4a95a9f15898f05e6cee264;hpb=10b525d1f3d4ffd1c95e8a0c3e580a64b0f20c5f;p=helm.git

diff --git a/helm/software/matita/library/Z/orders.ma b/helm/software/matita/library/Z/orders.ma
index c39f69308..0a3cfbe1f 100644
--- a/helm/software/matita/library/Z/orders.ma
+++ b/helm/software/matita/library/Z/orders.ma
@@ -68,7 +68,7 @@ interpretation "integer 'not less than'" 'nless x y =
   (cic:/matita/logic/connectives/Not.con (cic:/matita/Z/orders/Zlt.con x y)).
 
 theorem irreflexive_Zlt: irreflexive Z Zlt.
-change with (\forall x:Z. x < x \to False).
+unfold irreflexive.unfold Not.
 intro.elim x.exact H.
 cut (neg n < neg n \to False).
 apply Hcut.apply H.simplify.unfold lt.apply not_le_Sn_n.