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=15e58fd55809d51b2eee55ac68bc048d96ffc215;hpb=6604a232815858a6c75dd25ac45abd68438077ff;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 15e58fd55..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 *)
@@ -61,7 +61,7 @@ qed.
 
 (* Advanced constructions ***************************************************)
 
-(* yminus_O1 *)
+(*** yminus_O1 *)
 lemma ylminus_zero_sn (n): 𝟎 = 𝟎 - n.
 // qed.