proposition: Lemma iterate_S_eqn2 {A:Type}(f : A -> A) (n: nat)(x:A): iterate f (S n) x = (iterate f n (f x)).
proof: Proof. induction n. - reflexivity. - rewrite (iterate_S_eqn f (S n)), IHn; reflexivity. Qed.
imports: Coq(RelationClasses Relations Arith Max Lia) hydras(Exp2) LibHyps(LibHyps) hydras(MoreLibHyps)