proposition: Lemma iterate_comm {A: Type} f n (x:A) : iterate f n (f x) = f (iterate f n x).
proof: Proof. induction n; simpl. - trivial. - simpl; now f_equal. Qed.
imports: Coq(RelationClasses Relations Arith Max Lia) hydras(Exp2) LibHyps(LibHyps) hydras(MoreLibHyps)