proposition: Lemma sum_f_R0_ext : (sum_f_R0 An == sum_f_R0 Bn)%Rseq.
proof: Proof. intro n ; induction n ; simpl ; rewrite AnBn_ext ; [| rewrite IHn] ; reflexivity. Qed.
imports: Reals Rsequence_def Rpser_def Rpser_def_simpl Rpser_base_facts Rpser_sums Rpser_cv_facts Rinterval Ranalysis_def Rfunction_facts Tactics