proposition: Corollary iterate_ge_diag' : forall i f, dominates_from i f id-> strict_mono f -> forall n, {j:nat | i<= j /\ forall k, j<= k -> k <= iterate f n k}.
proof: Proof. intros; destruct n. - exists i; split;auto. - exists i; split; auto. intros. generalize (H k H1); intros. unfold id in H2, H; rewrite iterate_S_eqn. apply Nat.lt_le_incl. apply Nat.lt_le_trans with (f k); auto. apply mono_weak; auto. eapply iterate_ge_from with i; auto. Qed.
imports: Coq(RelationClasses Relations Arith Max Lia) hydras(Exp2) LibHyps(LibHyps) hydras(MoreLibHyps)