milestone update in ground, partial commit

[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 2df064a0189c3085ed0707a78532215d5e6bd79c..40beec972819238df4a5bdd75ed92e403d48d436 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 (non-negative integers)"
   'plus m n = (nplus m n).
 
 (* Basic constructions ******************************************************)
@@ -42,10 +42,12 @@ qed.
 (* Constructions with niter *************************************************)
 
 (*** iter_plus *)
-lemma niter_plus (A) (f) (a) (n1) (n2):
-      f^n1 (f^n2 a) = f^{A}(n1+n2) a.
-#A #f #a #n1 #n2 @(nat_ind_succ … n2) -n2 //
-#n2 #IH <nplus_succ_dx <niter_succ <niter_succ <niter_appl //
+lemma niter_plus (A) (f) (n1) (n2):
+      f^n2 ∘ f^n1 ≐ f^{A}(n1+n2).
+#A #f #n1 #n2 @(nat_ind_succ … n2) -n2 //
+#n2 #IH <nplus_succ_dx
+@exteq_repl
+/3 width=5 by compose_repl_fwd_sn, compose_repl_fwd_dx/
 qed.
 
 (* Advanved constructions (semigroup properties) ****************************)