proposition: Lemma Key : {t : IR | [0] [<=] t | forall J, {k : nat -> nat | (forall i, 1 <= k i /\ k i <= n) /\ (forall i, k (S i) <= k i) /\ (let k_0 := k 0 in a k_0[*]t[^]k_0 [=] a_0[-]eps) /\ (forall j, j <= J -> let k_j := k j in let r := t[*]p3m j in forall i, 1 <= i -> i <= n -> a i[*]r[^]i[-]eps [<=] a k_j[*]r[^]k_j)}}.
proof: Proof. Proof. elim lem_1. intro t. intros H0 H1. elim H1. intros k_0 H2. elim H2. intros H3 H4. elim H4. intros H5 H6. elim H6. intros H7 H8. clear H6 H4 H2 H1. exists t. auto. intro J. induction J as [| J HrecJ]. exists (fun j : nat => k_0). split. auto. split. auto. split. auto. intros j H9 k_j r i H10 H11. unfold k_j, r in |- *. rewrite (proj1 (Nat.le_0_r _) H9). replace (p3m 0) with OneR. 2: auto. astepr (a k_0[*] (t[^]k_0[*][1][^]k_0)). astepr (a k_0[*] (t[^]k_0[*][1])). astepr (a k_0[*]t[^]k_0). astepr (a_0[-]eps). apply minus_resp_leEq. astepl (a i[*] (t[^]i[*][1][^]i)). astepl (a i[*] (t[^]i[*][1])). astepl (a i[*]t[^]i); auto. elim HrecJ. intros k' H9. elim H9. intros H10 H11. elim H11. intros H12 H13. elim H13. intros H14 H15. clear H9 H11 H13. cut (0 < k' J). intro H16. 2: elim (H10 J); auto. elim (maj_upto_eps IR (fun i : nat => a i[*] (t[*]p3m (S J)) [^]i) ( k' J) Halfeps H16 Halfeps_pos). intros k_SJ H17. elim H17. intros H18 H19. elim H19. intros H20 H21. clear H17 H19. exists (chfun k' k_SJ J). split. intro i. apply chfun_3. auto. auto. apply Nat.le_trans with (k' J); auto. elim (H10 J). auto. split. intro i. apply chfun_4; auto. split. replace (chfun k' k_SJ J 0) with (k' 0); auto. intros j H22 k_j r i H23 H24. unfold k_j, r in |- *. elim (le_lt_eq_dec _ _ H22); intro H26. replace (chfun k' k_SJ J j) with (k' j). apply H15; auto with arith. apply chfun_1; auto with arith. replace (chfun k' k_SJ J j) with k_SJ. rewrite H26. elim (le_lt_dec i (k' J)); intro H28. apply Halfeps_eps. auto. apply Key_2 with (k' J) (a (k' J)); auto. apply chfun_2. rewrite H26. auto. Qed.
imports: Coq.ZArith.ZArith Coq.Arith.Compare CoRN.reals.NRootIR Coq(Lia)