proposition: Corollary iterate_ge_diag' : forall i f, f_gt_from i f -> mono f -> forall n, {j:nat | i<= j /\ forall k, j<= k -> k <= iterate f n k}.
proof: Proof. intros. destruct n. exists i. split;auto. exists i. split. auto. intros. red in H. red in H. generalize (H k H1); intros. unfold id_nat in H2, H. rewrite iterate_S_eqn. apply PeanoNat.Nat.lt_le_incl. apply Nat.lt_le_trans with (f k). auto. apply mono_weak. auto. eapply iterate_ge with i. red. red. unfold id_nat. apply H. auto. Qed.
imports: Coq(ArithRing Lia Arith)