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

diff --git a/matita/matita/contribs/lambdadelta/ground/arith/pnat_iter.ma b/matita/matita/contribs/lambdadelta/ground/arith/pnat_iter.ma
index a749c5339..49a51b0af 100644
--- a/matita/matita/contribs/lambdadelta/ground/arith/pnat_iter.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/pnat_iter.ma
@@ -15,8 +15,9 @@
 include "ground/notation/functions/exp_3.ma".
 include "ground/arith/pnat.ma".
 
-(* POSITIVE INTEGERS ********************************************************)
+(* ITERATED FUNCTION FOR POSITIVE INTEGERS **********************************)
 
+(* Note: see also: lib/arithemetics/bigops.ma *)
 rec definition piter (p:pnat) (A:Type[0]) (f:A→A) (a:A) ≝
 match p with
 [ punit   ⇒ f a
@@ -27,7 +28,7 @@ interpretation
   "iterated function (positive integers)"
   'Exp A f p = (piter p A f).
 
-(* Basic rewrites ***********************************************************)
+(* Basic constructions ******************************************************)
 
 lemma piter_unit (A) (f) (a): f a = (f^{A}𝟏) a.
 // qed.
@@ -35,7 +36,7 @@ lemma piter_unit (A) (f) (a): f a = (f^{A}𝟏) a.
 lemma piter_succ (A) (f) (p) (a): f (f^p a) = f^{A}(↑p) a.
 // qed.
 
-(* Advanced rewrites ********************************************************)
+(* Advanced constructions ***************************************************)
 
 lemma piter_appl (A) (f) (p) (a): f (f^p a) = f^{A}p (f a).
 #A #f #p elim p -p //