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=f8df1c6be9f171b1987ba7a493f344ce9e0c4521;hb=ab44166935d77276c04fcce50aa8281292776e29;hp=dd4fdcbf98a1e6e5c0667907c4c080c52b0c5696;hpb=7efb15b93cf42eae8b34a12a327ee7213c1dbecc;p=helm.git

diff --git a/helm/matita/library/nat/lt_arith.ma b/helm/matita/library/nat/lt_arith.ma
index dd4fdcbf9..f8df1c6be 100644
--- a/helm/matita/library/nat/lt_arith.ma
+++ b/helm/matita/library/nat/lt_arith.ma
@@ -116,7 +116,6 @@ qed.
 theorem lt_times_to_lt_l: 
 \forall n,p,q:nat. lt (times p (S n)) (times q (S n)) \to lt p q.
 intros.
-(* convertibility problem here *)
 cut Or (lt p q) (Not (lt p q)).
 elim Hcut.
 assumption.