X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Farith%2Fnat_plus.ma;h=d9c82ae33f9f8fdb05978cb80e1aa5b95ff68126;hp=75349d2da6281f130d0e2a0b3ea8930e379267f0;hb=68e028d053806177e218ee1a5f8778d3011bef83;hpb=ccf5878f2a2ec7f952f140e162391708a740517b

diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_plus.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_plus.ma
index 75349d2da..d9c82ae33 100644
--- a/matita/matita/contribs/lambdadelta/ground/arith/nat_plus.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_plus.ma
@@ -21,7 +21,7 @@ definition nplus: nat → nat → nat ≝
            λm,n. nsucc^n m.
 
 interpretation
-  "plus (positive integers"
+  "plus (positive integers)"
   'plus m n = (nplus m n).
 
 (* Basic rewrites ***********************************************************)
@@ -40,6 +40,7 @@ lemma nplus_succ_dx (m) (n): ↑(m+n) = m + ↑n.
 #m #n @(niter_succ … nsucc)
 qed.
 
+(*** plus_S1 *)
 lemma nplus_succ_sn (m) (n): ↑(m+n) = ↑m + n.
 #m #n @(niter_appl … nsucc)
 qed.