proposition: Lemma LF3 : F_ 3 >>s (fun n => iterate exp2 n n).
proof: Proof. red. destruct minoration as [x Hx]. assert (F_ 2 >>s id_nat). destruct (big_induction 2); auto. case H; intros; exists (max x0 (max x 1)). red; intros. assert (dominates_from j (F_ 2) exp2). { intros k Hk; apply Hx. transitivity j; eauto with arith. } generalize (L3 j H1). intros. specialize (H2 j). assert (0 < j) by eauto with arith. specialize (H2 H3). rewrite F_S_rw. apply Nat.le_lt_trans with ( iterate (F_ 2) j j). generalize (iterate_dom_prop exp2 (F_ 2) j); intro. assert (f_gt_from j (F_ 2)). { apply f_gt_from_le with x0; eauto with arith. } assert (mono (F_ 2)). { destruct (big_induction 2); now destruct p. } assert (dominates_from j (F_ 2) exp2). { assert (f_gt_from j exp2) . { apply f_gt_from_le with 0. auto with arith. intros z _. apply exp2_gt_id. } specialize (H4 H7 exp2_mono H6 H1 j); auto. } apply PeanoNat.Nat.lt_le_incl; eapply H4; auto. apply f_gt_from_le with 0; auto with arith. intros z _; apply exp2_gt_id. apply exp2_mono; auto. rewrite iterate_S_eqn. apply d. transitivity j. eauto with arith. apply iterate_ge with j; auto. apply f_gt_from_le with x0; auto. eauto with arith. Qed.
imports: Coq(ArithRing Lia Arith)