proposition: Lemma Main_1a : forall (r : IR) (k : nat), [0] [<=] r -> 1 <= k -> k <= n -> (forall i, 1 <= i -> i <= n -> a i[*] (r [/]ThreeNZ) [^]i[-]eps [<=] a k[*] (r [/]ThreeNZ) [^]k) -> let p_ := fun i : nat => a i[*]r[^]i in let p_k := a k[*]r[^]k in Sum 1 (pred k) p_ [<=] Half[*] ([1][-]Small) [*]p_k[+]Half[*]Three[^]n[*]eps.
proof: Proof. intros r k H H0 H1 H2 p_ p_k. unfold p_, p_k in |- *. apply leEq_transitive with (Sum 1 (pred k) (fun i : nat => Three[^]i[*] (a k[*] (r [/]ThreeNZ) [^]k[+]eps))). apply Sum_resp_leEq. auto with arith. intros i H3 H4. cut (Three[^]i [#] ZeroR). intro H5. apply shift_leEq_mult' with H5. apply nexp_resp_pos. apply pos_three. astepl (a i[*] (r[^]i[/] Three[^]i[//]H5)). astepl (a i[*] (r [/]ThreeNZ) [^]i). astepr (eps[+]a k[*] (r [/]ThreeNZ) [^]k). apply shift_leEq_plus'. apply H2. assumption. lia. apply nexp_resp_ap_zero. apply three_ap_zero. apply leEq_wdl with (Sum 1 (pred k) (fun i : nat => Three[^]i) [*] (a k[*] (r [/]ThreeNZ) [^]k[+]eps)). cut (Three[-][1] [#] ZeroR). intro H3. astepl ((Three[^]S (pred k) [-]Three[^]1[/] Three[-][1][//]H3) [*] (a k[*] (r [/]ThreeNZ) [^]k[+]eps)). rewrite -> (Nat.lt_succ_pred _ _ H0). astepl ((Three[^]k[-]Three[/] Three[-][1][//]H3) [*] (a k[*] (r [/]ThreeNZ) [^]k[+]eps)). rstepl ([1] [/]TwoNZ[*] (Three[^]k[-]Three) [*] (a k[*] (r [/]ThreeNZ) [^]k) [+] [1] [/]TwoNZ[*] (Three[^]k[-]Three) [*]eps). apply leEq_transitive with (Half[*] ([1][-]Small) [*] (a k[*]r[^]k) [+] [1] [/]TwoNZ[*] (Three[^]k[-]Three) [*]eps). apply plus_resp_leEq. cut (Three[^]k [#] ZeroR). intro H4. astepl ([1] [/]TwoNZ[*] (Three[^]k[-]Three) [*] (a k[*] (r[^]k[/] Three[^]k[//]H4))). rstepl ([1] [/]TwoNZ[*]a k[*]r[^]k[*] ([1][-] (Three[/] Three[^]k[//]H4))). rstepr (Half[*]a k[*]r[^]k[*] ([1][-]Small)). unfold Half in |- *. apply mult_resp_leEq_lft. apply minus_resp_leEq_both. apply leEq_reflexive. unfold Small in |- *. unfold p3m in |- *. cut (Three[^]pred k [#] ZeroR). intro H5. apply leEq_wdr with ([1][/] Three[^]pred k[//]H5). cut (Three[^]n [#] ZeroR). intro H6. astepl ([1][/] Three[^]n[//]H6). apply recip_resp_leEq. apply nexp_resp_pos. apply pos_three. apply great_nexp_resp_le. apply less_leEq; apply one_less_three. lia. apply nexp_resp_ap_zero. apply three_ap_zero. apply eq_div. pattern k at 1 in |- *. rewrite <- (Nat.lt_succ_pred _ _ H0). astepl ([1][*] (Three[*]Three[^]pred k):IR). clear H3 H4 H5. astepl ((Three[*]Three[^]pred k):IR). reflexivity. apply nexp_resp_ap_zero. apply three_ap_zero. apply mult_resp_nonneg. apply mult_resp_nonneg. apply less_leEq. astepr (Half:IR). apply pos_half. apply a_nonneg. apply nexp_resp_nonneg; auto. apply nexp_resp_ap_zero. apply three_ap_zero. apply plus_resp_leEq_lft. rstepl ([1] [/]TwoNZ[*]eps[*] (Three[^]k[-]Three)). rstepr (Half[*]eps[*]Three[^]n). unfold Half in |- *. apply mult_resp_leEq_lft. apply leEq_transitive with (Three[^]k:IR). astepr (Three[^]k[-]ZeroR). apply minus_resp_leEq_rht. apply less_leEq; apply pos_three. apply great_nexp_resp_le; auto. apply less_leEq; apply one_less_three. apply less_leEq; apply mult_resp_pos; auto. astepr (Half:IR); apply pos_half. rstepl (Two:IR). apply two_ap_zero. apply eq_symmetric_unfolded. apply mult_distr_sum_rht with (f := fun i : nat => (Three:IR) [^]i). Qed.
imports: CoRN.reals.CSumsReals CoRN.fta.KeyLemma CoRN.algebra.CRing_as_Ring Coq(Lia)