X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Flibrary%2Fnat%2Fminus.ma;h=063ab636ee8e3dae8096ba74817f48f838a98d6d;hb=cd91767a396b7bbc72e6e3ee90a3b758421f935d;hp=71c2cc20552a3c6474e93ab502232f3ed202e971;hpb=03d30a78581b24842e1f425b41861e5ae8f912b5;p=helm.git

diff --git a/matita/library/nat/minus.ma b/matita/library/nat/minus.ma
index 71c2cc205..063ab636e 100644
--- a/matita/library/nat/minus.ma
+++ b/matita/library/nat/minus.ma
@@ -140,8 +140,8 @@ intros 2.
 apply (nat_elim2 (\lambda n,m.n \leq m \to n-m = O)).
 intros.simplify.reflexivity.
 intros.apply False_ind.
-apply not_le_Sn_O.
-goal 13.apply H.
+apply not_le_Sn_O;
+[2: apply H | skip].
 intros.
 simplify.apply H.apply le_S_S_to_le. apply H1.
 qed.