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

diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_minus.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_minus.ma
index f386d413a..e4ccf83f4 100644
--- a/matita/matita/contribs/lambdadelta/ground/arith/nat_minus.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_minus.ma
@@ -19,10 +19,10 @@ include "ground/arith/nat_pred_succ.ma".
 
 (*** minus *)
 definition nminus: nat → nat → nat ≝
-           λm,n. npred^n m.
+           λm,n. (npred^n) m.
 
 interpretation
-  "minus (positive integers)"
+  "minus (non-negative integers)"
   'minus m n = (nminus m n).
 
 (* Basic constructions ******************************************************)
@@ -32,7 +32,7 @@ lemma nminus_zero_dx (m): m = m - 𝟎.
 // qed.
 
 (*** minus_SO_dx *)
-lemma nminus_one_dx (m): ↓m = m - 𝟏 .
+lemma nminus_unit_dx (m): ↓m = m - 𝟏 .
 // qed.
 
 (*** eq_minus_S_pred *)
@@ -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.