proposition: Lemma Rser_rem_ext: forall An l Hl Bn l' Hl' n, An == Bn -> Rser_rem An l Hl n = Rser_rem Bn l' Hl' n.
proof: Proof. intros ; apply Rminus_eq_compat ; [eapply Rser_cv_unique | eapply Rseq_sum_ext] ; [ | erewrite Rser_cv_ext |] ; eassumption. Qed.
imports: Rsequence Rseries_def Rseries_base_facts Rseries_cv_facts Rseries_pos_facts Lra MyRIneq