proposition: Lemma dominates_iterate : forall i f, dominates_from i f id -> strict_mono f -> forall n, {j:nat | i <= j /\ dominates_from j (iterate f (S n)) id}.
proof: Proof. induction n. exists i. split;auto. destruct IHn as [j [H1 H2]]. exists j. split;auto. red in H2; red. intros k Hk. unfold id. rewrite iterate_S_eqn. apply Nat.le_lt_trans with (f (iterate f n k)). apply Nat.le_trans with (iterate f n k). apply iterate_ge_from with i. auto. eauto with arith. apply PeanoNat.Nat.lt_le_incl. apply H. apply Nat.le_trans with k. eauto with arith. apply iterate_ge_from with i. auto. eauto with arith. apply H0. rewrite iterate_S_eqn. apply H. apply Nat.le_trans with k. eauto with arith. apply iterate_ge_from with i. auto. eauto with arith. Defined.
imports: Coq(RelationClasses Relations Arith Max Lia) hydras(Exp2) LibHyps(LibHyps) hydras(MoreLibHyps)