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 (compat "8.3").

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.