X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Farith%2Farith_2a.ma;fp=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Farith%2Farith_2a.ma;h=114eddb1e34837a19871dc0dffd802764e0abc54;hb=d85eac4e29291d854469e626381654181b0c7e87;hp=a136174bc8b209fc0c813c013b3382cdca587938;hpb=2815c74c03f38089d0e27aba00e2280223b0f76f;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/ground/arith/arith_2a.ma b/matita/matita/contribs/lambdadelta/ground/arith/arith_2a.ma
index a136174bc..114eddb1e 100644
--- a/matita/matita/contribs/lambdadelta/ground/arith/arith_2a.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/arith_2a.ma
@@ -24,7 +24,7 @@ lemma plus_n_2: ∀n. (n + 𝟐) = n + 𝟏 + 𝟏.
 // qed.
 
 lemma arith_b1: ∀a,b,c1. c1 ≤ b → a - c1 - (b - c1) = a - b.
-#a #b #c1 #H >nminus_comm <nminus_assoc_comm_23 //
+#a #b #c1 #H >nminus_comm_21 <nminus_assoc_comm_23 //
 qed-.
 
 lemma arith_b2: ∀a,b,c1,c2. c1 + c2 ≤ b → a - c1 - c2 - (b - c1 - c2) = a - b.