X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Farith%2Fnat_minus.ma;h=d975ff3bc59cdc6b145519090877d721d9c6f9dc;hp=f386d413ae67a0c1f0b7bc72be7a2e4e5098006f;hb=19b0a814861157ba05f23877d5cd94059f52c2e8;hpb=21de0d35017656c5a55528390b54b0b2ae395b44

diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_minus.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_minus.ma
index f386d413a..d975ff3bc 100644
--- a/matita/matita/contribs/lambdadelta/ground/arith/nat_minus.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_minus.ma
@@ -70,6 +70,11 @@ lemma nminus_succ_sn_refl (m): ninj (𝟏) = ↑m - m.
 qed.
 
 (*** minus_minus_comm *)
-lemma nminus_minus_comm (o) (m) (n): o - m - n = o - n - m.
+lemma nminus_comm (o) (m) (n): o - m - n = o - n - m.
 #o #m #n @(nat_ind_succ … n) -n //
-qed-.
+qed.
+
+(*** minus_minus_comm3 *)
+lemma nminus_comm_231 (n) (m1) (m2) (m3):
+      n-m1-m2-m3 = n-m2-m3-m1.
+// qed.