proposition: Corollary iterate_gt_diag' : forall i f, f_gt_from i f -> mono f -> forall n, 0 < n -> {j:nat | i<= j /\ f_gt_from j (iterate f n)}.
proof: Proof. intros. destruct n. - lia. - apply dominates_iterate; auto. Defined.
imports: Coq(ArithRing Lia Arith)