arithmetics for λδ

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

diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_minus.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_minus.ma
index f386d413ae67a0c1f0b7bc72be7a2e4e5098006f..d975ff3bc59cdc6b145519090877d721d9c6f9dc 100644 (file)
--- 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.