Much ado about nothing:

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

diff --git a/matita/library/nat/minus.ma b/matita/library/nat/minus.ma
index 71c2cc20552a3c6474e93ab502232f3ed202e971..063ab636ee8e3dae8096ba74817f48f838a98d6d 100644 (file)
--- 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.