proposition: Lemma Rser_rem_scal_compat_r: forall An l (k : R) Hlk Hl, Rser_rem (An * k) (l * k) Hlk == Rser_rem An l Hl * k.
proof: Proof. intros An l k Hlk Hl n ; unfold Rser_rem ; rewrite Rseq_sum_scal_compat_r ; unfold Rseq_plus, Rseq_minus, Rseq_constant, Rseq_mult ; ring. Qed.
imports: Rsequence Rseries_def Rseries_base_facts Rseries_cv_facts Rseries_pos_facts Lra MyRIneq