proposition: Lemma Main_1 : 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) -> (forall i, 1 <= i -> i <= n -> a i[*] (r[*]Three) [^]i[-]eps [<=] a k[*] (r[*]Three) [^]k) -> 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.
proof: Proof. intros r k H H0 H1 H2 H3 p_ p_k. unfold p_, p_k in |- *. set (h := Half[*] ([1][-]Small) [*]p_k[+]Half[*]Three[^]n[*]eps) in *. apply leEq_wdr with (h[+]h); unfold h, p_k in |- *. apply plus_resp_leEq_both. apply Main_1a; auto. apply Main_1b; auto. unfold Half in |- *; rational. Qed.
imports: CoRN.reals.CSumsReals CoRN.fta.KeyLemma CoRN.algebra.CRing_as_Ring Coq(Lia)