proposition: Lemma Rser_rem_minus_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_minus_compat ; unfold Rseq_plus, Rseq_minus ; ring. Qed.
imports: Rsequence Rseries_def Rseries_base_facts Rseries_cv_facts Rseries_pos_facts Lra MyRIneq