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