X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Farith%2Fynat_lminus.ma;h=b1dee6cef22a69780e78bbd0fdc10363812b4f6b;hb=0bcf2dc1a27e38cb6cd3d44eb838d652926841e0;hp=04cd607c9b2269c4317007342b06b3c85983dc33;hpb=4d232392091ee233afc26ecf3120dd5f5c6a33c8;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..b1dee6cef 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)"
@@ -42,7 +42,7 @@ lemma ylminus_succ_dx (x:ynat) (n): ↓(x-n) = x - ↑n.
 qed.
 
 (*** yminus_SO2 *)
-lemma ylminus_one_dx (x): ↓x = x - (𝟏).
+lemma ylminus_unit_dx (x): ↓x = x - (𝟏).
 // qed.
 
 (*** yminus_Y_inj *)