proposition: Lemma Rser_rem_cv : forall An l (Hl : Rser_cv An l ) (n : nat), Rser_cv (Rseq_shifts An (S n)) (Rser_rem An l Hl n).
proof: Proof. intros An l Hl n ; unfold Rser_cv ; eapply Rseq_cv_eq_compat. intro p ; eapply Rseq_sum_shifts_compat. unfold Rser_rem ; apply Rseq_cv_minus_compat. apply Rseq_cv_shifts_compat_reciprocal ; assumption. apply Rseq_constant_cv. Qed.
imports: Rsequence Rseries_def Rseries_base_facts Rseries_cv_facts Rseries_pos_facts Lra MyRIneq