Require Import Arith.
Open Scope nat_scope.

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