proposition: Lemma Rser_rem_opp_compat: forall An l Hl Hl2, Rser_rem (- An) (- l) Hl == - Rser_rem An l Hl2.
proof: Proof. intros An l Hl Hl2 n ; unfold Rser_rem ; rewrite Rseq_sum_opp_compat ; unfold Rseq_plus, Rseq_minus, Rseq_opp ; ring. Qed.
imports: Rsequence Rseries_def Rseries_base_facts Rseries_cv_facts Rseries_pos_facts Lra MyRIneq