X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Farith%2Fnat_iter.ma;h=7c883976c743d9fdd0295d19341b3242859ec056;hb=21de0d35017656c5a55528390b54b0b2ae395b44;hp=89c464804225a25d65e3d3ac5f00c1ac76dae44c;hpb=df7a2aa19e98dc28e7f22129275a175cead49e2d;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_iter.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_iter.ma
index 89c464804..7c883976c 100644
--- a/matita/matita/contribs/lambdadelta/ground/arith/nat_iter.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_iter.ma
@@ -15,8 +15,9 @@
 include "ground/arith/pnat_iter.ma".
 include "ground/arith/nat.ma".
 
-(* NON-NEGATIVE INTEGERS ****************************************************)
+(* ITERATED FUNCTION FOR NON-NEGATIVE INTEGERS ******************************)
 
+(*** iter *)
 definition niter (n:nat) (A:Type[0]) (f:A→A) (a:A) ≝
 match n with
 [ nzero  ⇒ a
@@ -28,16 +29,18 @@ interpretation
   "iterated function (non-negative integers)"
   'Exp A f n = (niter n A f).
 
-(* Basic rewrites ***********************************************************)
+(* Basic constructions ******************************************************)
 
+(*** iter_O *)
 lemma niter_zero (A) (f) (a): a = (f^{A}𝟎) a.
 // qed.
 
 lemma niter_inj (A) (f) (p) (a): f^p a = f^{A}(ninj p) a.
 // qed.
 
-(* Advanced rewrites ********************************************************)
+(* Advanced constructions ***************************************************)
 
+(*** iter_n_Sm *)
 lemma niter_appl (A) (f) (n) (a): f (f^n a) = f^{A}n (f a).
 #A #f * //
 #p #a <niter_inj <niter_inj <piter_appl //