proposition: Lemma Main : {r : IR | [0] [<=] r | {k : nat | 1 <= k /\ k <= n /\ (let p_ := fun i => a i[*]r[^]i in let p_k := a k[*]r[^]k in Sum 1 (pred k) p_[+]Sum (S k) n p_ [<=] ([1][-]Small) [*]p_k[+]Three[^]n[*]eps /\ r[^]n [<=] a_0 /\ Smaller[*]a_0[-]Two[*]eps [<=] p_k /\ p_k [<=] a_0)}}.
proof: Proof. Proof. elim (Key a n gt_n_0 eps eps_pos a_nonneg a_n_1 a_0 eps_le_a_0). intro t. intros H0 H1. elim (H1 two_n). intro k. intros H2. elim H2. intros H3 H4. elim H4. intros H5 H6. elim H6. intros H7 H8. elim (kseq_prop k n H3 H5). intro j. intros H9. elim H9. intros H10 H11. elim H11. intros H12 H13. clear H9 H6 H4 H2 H1. cut ([0] [<=] t[*]p3m (S j)). intro H14. 2: apply mult_resp_nonneg; auto. 2: apply less_leEq; apply p3m_pos. exists (t[*]p3m (S j)). auto. exists (k (S j)). elim (H3 (S j)); intros H3' H3''. split. auto. split. auto. intros p_ p_k. split; unfold p_, p_k in |- *. apply Main_1; auto. intros i H15 H16. apply Main_1a'; auto. intros i0 H17 H18. rewrite H13. apply H8; auto with arith. intros i H15 H16. apply Main_1b'; auto. intros i0 H17 H18. rewrite <- H12. apply H8; auto with arith. apply Nat.le_trans with (S j); auto with arith. split. astepl ([1][*] (t[*]p3m (S j)) [^]n). astepl (a n[*] (t[*]p3m (S j)) [^]n). apply Main_2 with (k 0); auto. intros i H15 H16. apply Main_2'. apply H8; auto with arith. elim (H3 0); intros H3''' H3''''. split. apply Main_3 with (k 0); auto. apply H8; auto with arith. apply Main_2 with (k 0); auto. intros i H15 H16. apply Main_2'; auto with arith. Qed.
imports: CoRN.reals.CSumsReals CoRN.fta.KeyLemma CoRN.algebra.CRing_as_Ring Coq(Lia)