proposition: Lemma iterate_dom_prop : forall f g i (Hgt : f_gt_from i f) (Hm : mono f) (Hm': 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; 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 with i. auto. auto. apply Hm'. assert (0 < S k) by auto with arith. specialize (IHk H0 l Hl). repeat rewrite iterate_S_eqn in IHk. auto. Qed.
imports: Coq(ArithRing Lia Arith)