proposition: 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.
proof: Proof. intros n A f x; case n; auto. - intros p _; unfold Z.iter, Z.abs_nat; apply Pos2Nat.inj_iter. - intros p abs; case abs; trivial. Qed.
imports: Wf_nat BinInt Zcompare Zorder Bool