update in ground

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

diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_plus.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_plus.ma
index 75ff371fb108a84e9847927ca670fd2af4c822f5..a9894fc6285e7aaf7ec746ddfebacb208b91885e 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/arith/nat_plus.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_plus.ma
@@ -18,7 +18,7 @@ include "ground/arith/nat_succ_iter.ma".
 
 (*** plus *)
 definition nplus: nat → nat → nat ≝
-           λm,n. nsucc^n m.
+           λm,n. (nsucc^n) m.
 
 interpretation
   "plus (non-negative integers)"
@@ -31,7 +31,7 @@ lemma nplus_zero_dx (m): m = m + 𝟎.
 // qed.
 
 (*** plus_SO_dx *)
-lemma nplus_one_dx (n): ↑n = n + 𝟏.
+lemma nplus_unit_dx (n): ↑n = n + 𝟏.
 // qed.
 
 (*** plus_n_Sm *)
@@ -57,7 +57,7 @@ lemma nplus_succ_sn (m) (n): ↑(m+n) = ↑m + n.
 #m #n @(niter_appl … nsucc)
 qed.
 
-(*** plus_O_n.con *)
+(*** plus_O_n *)
 lemma nplus_zero_sn (m): m = 𝟎 + m.
 #m @(nat_ind_succ … m) -m //
 qed.
@@ -76,7 +76,7 @@ qed.
 (* Helper constructions *****************************************************)
 
 (*** plus_SO_sn *)
-lemma nplus_one_sn (n): ↑n = 𝟏 + n.
+lemma nplus_unit_sn (n): ↑n = 𝟏 + n.
 #n <nplus_comm // qed.
 
 lemma nplus_succ_shift (m) (n): ↑m + n = m + ↑n.