arithmetics for λδ

[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 75349d2da6281f130d0e2a0b3ea8930e379267f0..d9c82ae33f9f8fdb05978cb80e1aa5b95ff68126 100644 (file)
--- 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.