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.

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.