* Obsolete debugging comments removed

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

diff --git a/helm/matita/library/nat/primes.ma b/helm/matita/library/nat/primes.ma
index d7ee89d4e5490fb2736c8b50597600927c137ac1..dc5f627e43103119199d71747a837c60b8595cf4 100644 (file)
--- a/helm/matita/library/nat/primes.ma
+++ b/helm/matita/library/nat/primes.ma
@@ -59,7 +59,7 @@ apply witness n m (div m n).
 rewrite > plus_n_O (n*div m n).
 rewrite < H1.
 rewrite < sym_times.
-(* perche' hint non lo trova ?*)
+(* Andrea: perche' hint non lo trova ?*)
 apply div_mod.
 assumption.
 qed.
@@ -116,10 +116,11 @@ apply lt_O_n_elim n2 Hcut.intro.rewrite < sym_times.
 simplify.rewrite < sym_plus.
 apply le_plus_n.
 elim le_to_or_lt_eq O n2.
-assumption.apply le_O_n.
+assumption.
 absurd O<m.assumption.
 rewrite > H2.rewrite < H3.rewrite < times_n_O.
 apply not_le_Sn_n O.
+apply le_O_n.
 qed.
 
 theorem divides_to_lt_O : \forall n,m. O < m \to divides n m \to O < n.