proposition: Lemma Rser_rem_equiv_compat : Un ~ Vn -> (Rser_rem Un lu Hlu) ~ (Rser_rem Vn lv Hlv).
proof: Proof. intro Heq. apply Rseq_equiv_sym. apply Rseq_equiv_sym in Heq. unfold Rseq_equiv in *. assert(Hrew : (Rser_rem Vn lv Hlv - Rser_rem Un lu Hlu)== Rser_rem (Vn-Un) (lv-lu) (Rser_cv_minus_compat Vn Un lv lu Hlv Hlu)). apply Rser_rem_minus_compat. intros eps Heps. destruct(Rser_rem_little_O_compat (Vn -Un) Vn Vn_pos (lv-lu) lv Hlv (Rser_cv_minus_compat Vn Un lv lu Hlv Hlu) Heq eps Heps) as [N HN]. exists N. intro n. rewrite Hrew. apply HN. Qed.
imports: Reals Rsequence Rseries_def Rseries_base_facts Rseries_pos_facts Rseries_remainder_facts Rseries_cv_facts Rseries_usual Lra PeanoNat Rtactic MyRIneq