milestone update in ground

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

diff --git a/matita/matita/contribs/lambdadelta/ground/arith/ynat_lminus.ma b/matita/matita/contribs/lambdadelta/ground/arith/ynat_lminus.ma
index 04cd607c9b2269c4317007342b06b3c85983dc33..6a2e4dbeeb091bdd3ad4ea1580f85d7cc9a46b86 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/arith/ynat_lminus.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/ynat_lminus.ma
@@ -19,7 +19,7 @@ include "ground/arith/ynat_pred.ma".
 
 (*** yminus_sn *)
 definition ylminus (x) (n): ynat ≝
-           ypred^n x.
+           (ypred^n) x.
 
 interpretation
   "left minus (non-negative integers with infinity)"