Library Coq.ZArith.Zmisc
Require Import Wf_nat.
Require Import BinInt.
Require Import Zcompare.
Require Import Zorder.
Require Import Bool.
Local Open Scope Z_scope.
Iterators
nth iteration of the function f
Notation iter := @Z.iter (only parsing).
Lemma iter_nat_of_Z : forall n A f x, 0 <= n ->
Z.iter n f x = iter_nat (Z.abs_nat n) A f x.