X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Farith%2Fnat_plus.ma;h=f1dffc51db7350cba1caaa9c66113607bd0ae695;hb=55c768d7e45babb300b5010463ba3196a68f1bbe;hp=75ff371fb108a84e9847927ca670fd2af4c822f5;hpb=15212e44902f25536f6e2de4bec4cedcd9a9804d;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_plus.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_plus.ma
index 75ff371fb..f1dffc51d 100644
--- 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)"
@@ -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.