More notation here and there.

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

diff --git a/helm/matita/library/nat/lt_arith.ma b/helm/matita/library/nat/lt_arith.ma
index 19f25a967c0376dd2045007c67145c175ad94ed7..a2e7f6109af689edeb6e87fe5f09345e4ea706f8 100644 (file)
--- a/helm/matita/library/nat/lt_arith.ma
+++ b/helm/matita/library/nat/lt_arith.ma
@@ -116,7 +116,7 @@ qed.
 theorem lt_times_to_lt_l: 
 \forall n,p,q:nat. p*(S n) < q*(S n) \to p < q.
 intros.
-cut p < q \lor \lnot (p < q).
+cut p < q \lor p \nlt q.
 elim Hcut.
 assumption.
 absurd p * (S n) < q * (S n).