X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Farith%2Fynat_lminus.ma;h=6a2e4dbeeb091bdd3ad4ea1580f85d7cc9a46b86;hb=55c768d7e45babb300b5010463ba3196a68f1bbe;hp=04cd607c9b2269c4317007342b06b3c85983dc33;hpb=15212e44902f25536f6e2de4bec4cedcd9a9804d;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/ground/arith/ynat_lminus.ma b/matita/matita/contribs/lambdadelta/ground/arith/ynat_lminus.ma
index 04cd607c9..6a2e4dbee 100644
--- 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)"