proposition: Lemma iterate_compat3 f x n : iterate f n x = nat_rec (fun _ : nat => nat) x (fun _ y : nat => f y) n.
proof: Proof. induction n;cbn; auto. Qed.
imports: Coq(RelationClasses Relations Arith Max Lia) hydras(Exp2) LibHyps(LibHyps) hydras(MoreLibHyps)