proposition: Lemma Rser_rem_plus_compat: forall An Bn la lb Hla Hlb Hlab, Rser_rem An la Hla + Rser_rem Bn lb Hlb == Rser_rem (An + Bn) (la + lb) Hlab.
proof: Proof. intros An Bn la lb Hla Hlb Hlab n ; unfold Rser_rem ; rewrite Rseq_sum_plus_compat ; unfold Rseq_plus, Rseq_minus ; ring. Qed.
imports: Rsequence Rseries_def Rseries_base_facts Rseries_cv_facts Rseries_pos_facts Lra MyRIneq