proposition: Lemma dominates_iterate : forall i f, f_gt_from i f -> mono f -> forall n, {j:nat | i<= j /\ f_gt_from j (iterate f (S n))}.
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_nat. 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 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 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 with i. auto. eauto with arith. Defined.
imports: Coq(ArithRing Lia Arith)