update in ground

[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..e4ccf83f4f4b5265f3e11c4874523dbdda5f98c0 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 *)