* Obsolete debugging comments removed

[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 dd4fdcbf98a1e6e5c0667907c4c080c52b0c5696..f8df1c6be9f171b1987ba7a493f344ce9e0c4521 100644 (file)
--- 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.