proposition: Lemma sum_f_R0_Ropp_compat : forall An n, - sum_f_R0 An n = sum_f_R0 (-An)%Rseq n.
proof: Proof. intros An n ; induction n. reflexivity. simpl ; rewrite Ropp_plus_distr ; rewrite IHn ; reflexivity. Qed.
imports: Reals MyReals Rsequence_def Rsequence_facts Rsequence_sums_facts Rseries_def Rpser_def Rpser_sums Rpser_sums_facts Rpser_derivative Rpser_radius_facts Rpser_taylor Lra Rintegral Rseries_facts Rseries_RiemannInt Rsequence_subsequence Rtactic