proposition: Lemma iterate_nat_rec (g: nat->nat) (n:nat) x : iterate g n x = nat_rec (fun _ => nat) x (fun x y => g y) n.
proof: Proof. induction n; cbn; auto. Qed.
imports: hydras(primRec Ack MoreVectors) Coq(Arith ArithRing List Lia Compare_dec)