proposition: Lemma Rser_Rser_rem_equiv: forall An Bn x l (H : Rser_cv Bn l) n, (forall k, An k = Rseq_shifts Bn (S n) k) -> Rser_cv An x -> x = Rser_rem Bn l H n.
proof: Proof. intros An Bn x l Hl n Heq Hx ; eapply Rser_cv_unique. apply Hx. eapply Rser_cv_ext with (Rseq_shifts Bn (S n)). intro ; apply Heq. apply Rser_cv_shifts ; assumption. Qed.
imports: Rsequence Rseries_def Rseries_base_facts Rseries_cv_facts Rseries_pos_facts Lra MyRIneq