proposition: Lemma Telescoping_series_opp : forall a n, sum_f_R0 (fun i => a i - a (S i)) n = a O - a (S n).
proof: Proof. intros a n. rewrite tech11 with (fun i => a i - a (S i)) a (fun i => a (S i)) _; [|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' -> A + S - (S' + B) = 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