update in ground

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

diff --git a/matita/matita/contribs/lambdadelta/ground/arith/ynat_plus.ma b/matita/matita/contribs/lambdadelta/ground/arith/ynat_plus.ma
index f76cbc115bb118588de873b61010498f0680be55..f002081e4f1bc0cc2de4a6c9bb70b3a2c31db463 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/arith/ynat_plus.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/ynat_plus.ma
@@ -19,7 +19,7 @@ include "ground/arith/ynat_succ.ma".
 (* ADDITION FOR NON-NEGATIVE INTEGERS WITH INFINITY *************************)
 
 definition yplus_aux (x) (n): ynat ≝
-           ysucc^n x.
+           (ysucc^n) x.
 
 (*** yplus *)
 definition yplus (x): ynat → ynat ≝
@@ -32,7 +32,7 @@ interpretation
 (* Basic constructions ******************************************************)
 
 lemma yplus_inj_dx (x) (n):
-      ysucc^n x = x + yinj_nat n.
+      (ysucc^n) x = x + yinj_nat n.
 #x @(ynat_bind_nat_inj (yplus_aux x))
 qed.
 
@@ -47,7 +47,7 @@ lemma yplus_zero_dx (x): x = x + 𝟎.
 (* Constructions with ysucc *************************************************)
 
 (*** yplus_SO2 *)
-lemma yplus_one_dx (x): ↑x = x + 𝟏.
+lemma yplus_unit_dx (x): ↑x = x + 𝟏.
 // qed.
 
 (*** yplus_S2 yplus_succ2 *)