proposition: Lemma Kneser_3 : {z : CC | AbsCC z[^]n [<=] c | AbsCC (Sum 0 n (fun i => b i[*]z[^]i)) [<] q[*]c}.
proof: Proof. elim eta_exists. intros eta H0 H1. elim H1. intros b_0' H3 H4. elim H4. intros H5 H6. clear H1 H4. cut ([0] [<] AbsCC b_0'). intro H7. 2: apply AbsCC_pos; auto. elim (eps_exists eta (AbsCC b_0') H0 H7). intros eps H9 H10. elim H10. intros H11 H12. elim H12. intros H13 H14. clear H10 H12. cut (forall k : nat, [0] [<=] a k). intro H15. 2: intro; unfold a in |- *; apply AbsCC_nonneg. cut (a n [=] [1]). intro H16. 2: unfold a in |- *; Step_final (AbsCC [1]). elim (Main a n gt_n_0 eps H9 H15 H16 (AbsCC b_0') H14). intro r. intros H18 H19. elim H19. intros k H20. elim H20. intros H21 H22. elim H22. intros H23 H24. elim H24. intros H25 H26. elim H26. intros H27 H28. elim H28. intros H29 H30. clear H19 H20 H22 H24 H26 H28. cut ([0] [<] a k). intro H31. elim (z_exists b_0' k r eta H7 H31 H21 H23 H18 H0 H3 H30). intro z. intros H33 H34. exists z. astepl (r[^]n). apply leEq_transitive with (AbsCC b_0'); auto. apply leEq_transitive with (AbsCC b_0'[+]Three[*]eta). 2: apply less_leEq; auto. astepl (AbsCC b_0'[+][0]). apply plus_resp_leEq_lft. apply less_leEq. apply mult_resp_pos; auto. apply pos_three. set (r' := AbsCC z) in *. unfold r' in H33, H34. set (p_' := fun i : nat => a i[*]r'[^]i) in *. apply leEq_less_trans with (eps[+] (q[*]AbsCC b_0'[+]Three[^]n[*]eps[+]eta)). 2: rstepl (q[*]AbsCC b_0'[+]Three[^]n[*]eps[+]eps[+]eta); apply Kneser_1; auto. apply leEq_transitive with (AbsCC (b_0[+]b k[*]z[^]k) [+] (Sum 1 (pred k) p_'[+]Sum (S k) n p_')); unfold p_', r' in |- *. apply Kneser_2; auto. set (p_'' := fun i : nat => a i[*]r[^]i) in *. apply leEq_wdl with (AbsCC (b_0[+]b k[*]z[^]k) [+] (Sum 1 (pred k) p_''[+]Sum (S k) n p_'')); unfold p_'' in |- *. 2: apply bin_op_wd_unfolded; [ algebra | apply bin_op_wd_unfolded; apply Sum_wd; algebra ]. apply leEq_transitive with (AbsCC (b_0[+]b k[*]z[^]k) [+] (([1][-]Small) [*] (a k[*]r[^]k) [+]Three[^]n[*]eps)). apply plus_resp_leEq_lft; auto. apply leEq_transitive with (AbsCC b_0'[-]AbsCC (b k) [*]r[^]k[+]eta[+] (([1][-]Small) [*] (a k[*]r[^]k) [+]Three[^]n[*]eps)). apply plus_resp_leEq; auto. unfold a in |- *. rstepl (AbsCC b_0'[+]Three[^]n[*]eps[+]eta[-]Small[*] (AbsCC (b k) [*]r[^]k)). apply leEq_transitive with (AbsCC b_0'[+]Three[^]n[*]eps[+]eta[-] Small[*] (Smaller[*]AbsCC b_0'[-]Two[*]eps)). apply minus_resp_leEq_rht. apply mult_resp_leEq_lft; auto. unfold Small in |- *. apply less_leEq; apply p3m_pos. apply leEq_wdl with (Small[*]Two[*]eps[+] (q[*]AbsCC b_0'[+]Three[^]n[*]eps[+]eta)). 2: unfold q, Smallest in |- *; rational. apply plus_resp_leEq. astepr ([1][*]eps). apply mult_resp_leEq_rht. 2: apply less_leEq; auto. astepr (Half[*] (Two:IR)). apply mult_resp_leEq_rht. unfold Small in |- *; apply p3m_smaller; auto. apply less_leEq; apply pos_two. apply mult_cancel_pos_lft with (r[^]k). 2: apply nexp_resp_nonneg; auto. apply less_leEq_trans with eps; auto. eapply leEq_transitive. 2: apply H29. apply shift_leEq_minus. rstepl (Three[*]eps). auto. Qed.
imports: CoRN.complex.NRootCC CoRN.complex.AbsCC CoRN.fta.MainLemma