proposition: Lemma lem_1 : {t : IR | [0] [<=] t | {k : nat | 1 <= k /\ k <= n /\ a k[*]t[^]k [=] a_0[-]eps /\ (forall i, 1 <= i -> i <= n -> a i[*]t[^]i [<=] a_0)}}.
proof: Proof. cut (forall j : nat, let l := n - j in 1 <= l -> l <= n -> {t : IR | [0] [<=] t | {k : nat | l <= k /\ k <= n /\ a k[*]t[^]k [=] a_0[-]eps /\ (forall i : nat, l <= i -> i <= n -> a i[*]t[^]i [<=] a_0)}}). intro H. rewrite <- lem_1a. apply H; rewrite lem_1a; auto with arith. intro j. induction j as [| j Hrecj]. replace (n - 0) with n. 2: auto with arith. intros l H H0. exists (NRoot a_0_eps_nonneg gt_n_0). apply NRoot_nonneg. exists n. split. auto. split. auto. split. astepl ([1][*]NRoot a_0_eps_nonneg gt_n_0[^]n). Step_final (NRoot a_0_eps_nonneg gt_n_0[^]n). intros i H1 H2. replace i with n. 2: apply Nat.le_antisymm; auto. astepl ([1][*]NRoot a_0_eps_nonneg gt_n_0[^]n). astepl (NRoot a_0_eps_nonneg gt_n_0[^]n). astepl (a_0[-]eps). apply less_leEq; apply a_0_eps_fuzz. intros l H H0. cut (1 <= n - j). intro H1. 2: apply Nat.le_trans with (n - S j); [ auto | apply lem_1b ]. cut (n - j <= n). intro H2. 2: apply lem_1c. elim (Hrecj H1 H2). intros t' H4 H5. elim H5. intros k' H6. elim H6. intros H7 H8. elim H8. intros H9 H10. elim H10. intros H11 H12. clear H10 H8 H6 H5. elim (less_cotransitive_unfolded _ _ _ a_0_eps_fuzz (a (n - S j) [*]t'[^] (n - S j))); intro H14. cut ([0] [<] a (n - S j)). intro H15. cut (a (n - S j) [#] [0]). intro H16. 2: apply pos_ap_zero; auto. cut ([0] [<=] (a_0[-]eps[/] a (n - S j) [//]H16)). intro H17. cut (0 < n - S j). intro H18. 2: auto with arith. exists (NRoot H17 H18). apply NRoot_nonneg. exists (n - S j). split. auto. split. auto. split. astepl (a (n - S j) [*] (a_0[-]eps[/] a (n - S j) [//]H16)). rational. intros i H19 H20. elim (le_lt_eq_dec _ _ H19); intro H22. apply leEq_transitive with (a i[*]t'[^]i). apply mult_resp_leEq_lft. apply power_resp_leEq. apply NRoot_nonneg. apply power_cancel_leEq with (n - S j); auto. astepl (a_0[-]eps[/] a (n - S j) [//]H16). apply shift_div_leEq. auto. astepr (a (n - S j) [*]t'[^] (n - S j)). apply less_leEq; auto. apply a_nonneg. apply H12. replace (n - j) with (S (n - S j)); [auto with arith|]. rewrite <- Nat.sub_succ_l; auto with arith. auto. rewrite <- H22. astepl (a (n - S j) [*] (a_0[-]eps[/] a (n - S j) [//]H16)). astepl (a_0[-]eps). apply less_leEq; apply a_0_eps_fuzz. apply shift_leEq_div; auto. astepl ZeroR; apply a_0_eps_nonneg. cut ([0] [<] a (n - S j) [*]t'[^] (n - S j)). intro H15. 2: apply leEq_less_trans with (a_0[-]eps); auto. 2: apply a_0_eps_nonneg. apply leEq_not_eq. apply a_nonneg. apply ap_symmetric_unfolded. exact (cring_mult_ap_zero _ _ _ (pos_ap_zero _ _ H15)). exists t'. auto. exists k'. split. apply Nat.le_trans with (n - j). unfold l in |- *; apply lem_1b. auto. split. auto. split. auto. intros i H15 H16. elim (le_lt_eq_dec _ _ H15); intro H18. apply H12. replace (n - j) with (S (n - S j)); [auto with arith|]. rewrite <- Nat.sub_succ_l; auto with arith. auto. rewrite <- H18. apply less_leEq; auto. Qed.
imports: Coq.ZArith.ZArith Coq.Arith.Compare CoRN.reals.NRootIR Coq(Lia)