X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Flibrary%2Fnat%2Flt_arith.ma;fp=helm%2Fmatita%2Flibrary%2Fnat%2Flt_arith.ma;h=a2e7f6109af689edeb6e87fe5f09345e4ea706f8;hb=73e63e535940a068e660d3688a3c8ebfa1930561;hp=19f25a967c0376dd2045007c67145c175ad94ed7;hpb=30b7e65d641fe7243c4f36ed448f56360a1c5e1c;p=helm.git

diff --git a/helm/matita/library/nat/lt_arith.ma b/helm/matita/library/nat/lt_arith.ma
index 19f25a967..a2e7f6109 100644
--- 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).