arithmetics for λδ

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

diff --git a/matita/matita/contribs/lambdadelta/ground/arith/pnat_plus.ma b/matita/matita/contribs/lambdadelta/ground/arith/pnat_plus.ma
index eead7943bb2a50d4859b90c3cb6ff2aad0719f63..53d5236f340fa4d455dcb2fa7eda3c904b00f390 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/arith/pnat_plus.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/pnat_plus.ma
@@ -14,7 +14,7 @@
 
 include "ground/arith/pnat_iter.ma".
 
-(* POSITIVE INTEGERS ********************************************************)
+(* ADDITION FOR POSITIVE INTEGERS *******************************************)
 
 definition pplus: pnat → pnat → pnat ≝
            λp,q. psucc^q p.
@@ -31,7 +31,7 @@ lemma pplus_one_dx (p): ↑p = p + 𝟏.
 lemma pplus_succ_dx (p) (q): ↑(p+q) = p + ↑q.
 // qed.
 
-(* Semigroup properties *****************************************************)
+(* Advanced reweites (semigroup properties) *********************************)
 
 lemma pplus_succ_sn (p) (q): ↑(p+q) = ↑p + q.
 #p #q @(piter_appl … psucc)