Library Coqtail.Arith.Ntools


Require Import Arith.
Open Scope nat_scope.

Iteration of a function over nat


Fixpoint iter_nat (n:nat) (A:Type) (f:natAA) (x:A) {struct n} : A :=
  match n with
    | 0 ⇒ x
    | S n'f n (iter_nat n' A f x)
  end.