update from master branch

[helm.git] / matita / matita / contribs / lambdadelta / ground / arith / nat_minus_plus.ma

diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_minus_plus.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_minus_plus.ma
index e910fdaa0c94802be4767ba40f7e13a349951a46..97c24dbd470ae51b1eb17bb778a677f5df40dfa8 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/arith/nat_minus_plus.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_minus_plus.ma
@@ -38,7 +38,7 @@ qed.
 
 (*** minus_plus_plus_l *)
 lemma nminus_plus_dx_bi (m) (n) (o): m - n = (m + o) - (n + o).
-#m #n #o <nminus_plus_assoc <nminus_comm //
+#m #n #o <nminus_plus_assoc <nminus_comm_21 //
 qed.
 
 (* Helper constructions with nplus ******************************************)