proposition: Lemma Rser_rem_scal_compat_l: forall An l (k : R) Hkl Hl, Rser_rem (k * An) (k * l) Hkl == k * Rser_rem An l Hl.
proof: Proof. intros An l k Hkl Hl n ; unfold Rser_rem ; rewrite Rseq_sum_scal_compat_l ; 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