(* 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
"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.
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 //