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..b1dee6cef22a69780e78bbd0fdc10363812b4f6b 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)"
@@ -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 *)