proposition: Lemma iterate_lt f (Hf : strict_mono f)(Hf': fun_le S f): forall i j, i < j -> forall z, iterate f i z < iterate f j z.
proof: Proof. induction 1. - intros; rewrite iterate_S_eqn; auto. - intros; rewrite iterate_S_eqn; transitivity (iterate f m z); auto. Qed.
imports: Coq(RelationClasses Relations Arith Max Lia) hydras(Exp2) LibHyps(LibHyps) hydras(MoreLibHyps)