proposition: Lemma iterate_rw {A} {f : A -> A} n : forall x, iterate f (S n) x = iterate f n (f x).
proof: Proof. simpl; induction n. - reflexivity. - intros; simpl; now f_equal. Qed.
imports: Coq(RelationClasses Relations Arith Max Lia) hydras(Exp2) LibHyps(LibHyps) hydras(MoreLibHyps)