X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Farith%2Fpnat_plus.ma;h=c5c6ade72cc63a23b7e66a659590000f3cc2e327;hp=e6db03ac46b8cccce12764f84693c9a8e461dc74;hb=21de0d35017656c5a55528390b54b0b2ae395b44;hpb=68e028d053806177e218ee1a5f8778d3011bef83

diff --git a/matita/matita/contribs/lambdadelta/ground/arith/pnat_plus.ma b/matita/matita/contribs/lambdadelta/ground/arith/pnat_plus.ma
index e6db03ac4..c5c6ade72 100644
--- a/matita/matita/contribs/lambdadelta/ground/arith/pnat_plus.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/pnat_plus.ma
@@ -23,7 +23,7 @@ interpretation
   "plus (positive integers)"
   'plus p q = (pplus p q).
 
-(* Basic rewrites ***********************************************************)
+(* Basic constructions ******************************************************)
 
 lemma pplus_one_dx (p): ↑p = p + 𝟏.
 // qed.
@@ -31,7 +31,7 @@ lemma pplus_one_dx (p): ↑p = p + 𝟏.
 lemma pplus_succ_dx (p) (q): ↑(p+q) = p + ↑q.
 // qed.
 
-(* Advanced reweites (semigroup properties) *********************************)
+(* Advanced constructions (semigroup properties) ****************************)
 
 lemma pplus_succ_sn (p) (q): ↑(p+q) = ↑p + q.
 #p #q @(piter_appl … psucc)
@@ -43,7 +43,7 @@ qed.
 
 lemma pplus_comm: commutative … pplus.
 #p elim p -p //
-qed.
+qed-.
 
 lemma pplus_assoc: associative … pplus.
 #p #q #r elim r -r //