Library Stdlib.ZArith.Zmisc

From Stdlib Require Import Wf_nat.
From Stdlib Require Import BinInt.
From Stdlib Require Import Zcompare.
From Stdlib Require Import Zorder.
From Stdlib 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.