More commands documented.

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

diff --git a/matita/library/nat/orders.ma b/matita/library/nat/orders.ma
index 6ec0c9992a68b18e15976e96e74ef853c2fc04eb..312487055e8f7a9442c3c7ab6050aaa89ab1635d 100644 (file)
--- 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.