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