proposition: Lemma iterate_dom_prop : forall f g i (Hgt : S <<= f) (Hm : strict_mono f) (Hm': strict_mono g), dominates_from i g f -> forall k, 0 < k -> dominates_from i (iterate g k) (iterate f k).
proof: Proof. induction k. - intro H0; inversion H0. - destruct k. + simpl; intros _ l Hl; apply H; auto. + intros _ l Hl; {autorename}. repeat rewrite iterate_S_eqn. transitivity (g (f (iterate f k l))). * apply H; transitivity (f l). { transitivity l; auto. apply PeanoNat.Nat.lt_le_incl. eapply Hgt; auto. } apply mono_weak; auto. eapply iterate_ge; auto. * apply Hm'; assert (0 < S k)%nat by auto with arith. apply IHk in H0; specialize (H0 l). repeat rewrite iterate_S_eqn in H0; auto. Qed.
imports: Coq(RelationClasses Relations Arith Max Lia) hydras(Exp2) LibHyps(LibHyps) hydras(MoreLibHyps)