Library hydras.MoreAck.Iterate_compat

From hydras Require primRec Iterates.
From hydras.Ackermann Require Import extEqualNat.


Lemma iterate_compat (f: nat → nat) n x :
  Iterates.iterate f n x = primRec.iterate f n x.

Lemma iterate_extEqual (f: nat → nat) n :
  extEqual 1 (Iterates.iterate f n) (primRec.iterate f n).