* Obsolete debugging comments removed

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

diff --git a/helm/matita/library/nat/minus.ma b/helm/matita/library/nat/minus.ma
index 079e902ad39ba9213b28b7b58062ed9e9db39dcb..7240b7d09ebbc9f18384e68ae1d51f3dffa8021b 100644 (file)
--- a/helm/matita/library/nat/minus.ma
+++ b/helm/matita/library/nat/minus.ma
@@ -118,8 +118,8 @@ intros 2.
 apply nat_elim2 (\lambda n,m.n \leq m \to n-m = O).
 intros.simplify.reflexivity.
 intros.apply False_ind.
-(* ancora problemi con il not *)
-apply not_le_Sn_O n1 H.
+apply not_le_Sn_O.
+goal 13.apply H.
 intros.
 simplify.apply H.apply le_S_S_to_le. apply H1.
 qed.