update from master branch

[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 5d3726ca85c53b1dd16a30d5c7891079a3b51098..6f11682723d94fdf4444c10e258363335538e9d8 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/arith/nat_minus.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_minus.ma
@@ -19,7 +19,7 @@ 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 (non-negative integers)"
@@ -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,11 +70,11 @@ lemma nminus_succ_sn_refl (m): ninj (𝟏) = ↑m - m.
 qed.
 
 (*** minus_minus_comm *)
-lemma nminus_comm (o) (m) (n): o - m - n = o - n - m.
-#o #m #n @(nat_ind_succ … n) -n //
+lemma nminus_comm_21 (m) (n1) (n2): m - n1 - n2 = m - n2 - n1.
+#m #n1 #n2 @(nat_ind_succ … n2) -n2 //
 qed.
 
 (*** minus_minus_comm3 *)
-lemma nminus_comm_231 (n) (m1) (m2) (m3):
-      n-m1-m2-m3 = n-m2-m3-m1.
+lemma nminus_comm_231 (m) (n1) (n2) (n3):
+      m-n1-n2-n3 = m-n2-n3-n1.
 // qed.