proposition: Lemma Telescoping_series : forall a n, sum_f_R0 (fun i => a (S i) - a i) n = a (S n) - a O.
proof: Proof. intros a n. rewrite tech11 with (fun i => a (S i) - a i) (fun i => a (S i)) a _; [|reflexivity]. destruct n; [reflexivity|]. rewrite tech2 with a O (S n); [|intuition]. rewrite tech5. simpl (sum_f_R0 a 0). replace (S n - 1)%nat with n by (simpl; symmetry; apply Nat.sub_0_r). assert (REW : forall S S' A B, S = S' -> S + A - (B + S') = A - B) by (intros; subst; ring). apply REW. reflexivity. Qed.
imports: Reals Rseries_def Rseries_facts RiemannInt Lra Rsequence_facts Rsequence_subsequence Riemann_integrable Rintegral