X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Flibrary%2Fnat%2Forders.ma;h=312487055e8f7a9442c3c7ab6050aaa89ab1635d;hb=b473a681dfab815f882bc646efc2b218f1957db8;hp=6ec0c9992a68b18e15976e96e74ef853c2fc04eb;hpb=7f2444c2670cadafddd8785b687ef312158376b0;p=helm.git

diff --git a/matita/library/nat/orders.ma b/matita/library/nat/orders.ma
index 6ec0c9992..312487055 100644
--- a/matita/library/nat/orders.ma
+++ b/matita/library/nat/orders.ma
@@ -163,8 +163,7 @@ apply not_le_to_lt.exact H.
 qed.
 
 theorem le_to_not_lt: \forall n,m:nat. le n m \to Not (lt m n).
-intros.
-change with (Not (le (S m) n)).
+intros.unfold Not.unfold lt.
 apply lt_to_not_le.unfold lt.
 apply le_S_S.assumption.
 qed.