X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Flibrary%2Fnat%2Fminus.ma;h=7240b7d09ebbc9f18384e68ae1d51f3dffa8021b;hb=ab44166935d77276c04fcce50aa8281292776e29;hp=079e902ad39ba9213b28b7b58062ed9e9db39dcb;hpb=7efb15b93cf42eae8b34a12a327ee7213c1dbecc;p=helm.git

diff --git a/helm/matita/library/nat/minus.ma b/helm/matita/library/nat/minus.ma
index 079e902ad..7240b7d09 100644
--- 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.