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=775ab35f714568dfcd672f0dd53a00e1ba7382cd;hp=5d3726ca85c53b1dd16a30d5c7891079a3b51098;hpb=888840f6b3a71d3d686b53b702d362ab90ab0038;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 5d3726ca8..e4ccf83f4 100644
--- 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 *)