proposition: Lemma iterate_lt_from f k: strict_mono f -> ( forall n, k <= n -> n < f n) -> forall i j : nat, i < j -> forall z : nat, k <= z -> iterate f i z < iterate f j z.
proof: Proof. induction 3 /r. - intros Hmono Hind * Hkz; rewrite iterate_S_eqn; auto. apply Hind; revert i; induction i /r. + cbn; auto. + transitivity (iterate f i z); auto. rewrite iterate_S_eqn; apply Nat.lt_le_incl. apply Hind; auto. - intros Hmono Hind * Hlt Hind2 * Kkz; transitivity (iterate f m z); auto. rewrite iterate_S_eqn; apply Hind. transitivity z; auto. clear i Hlt Hind2; induction m. + cbn; auto. + cbn; transitivity (iterate f m z); auto. apply Nat.lt_le_incl, Hind; lia. Qed.
imports: Coq(RelationClasses Relations Arith Max Lia) hydras(Exp2) LibHyps(LibHyps) hydras(MoreLibHyps)