proposition: Lemma Rser_cv_zero : forall An l, Rser_cv An l -> Rseq_cv An 0.
proof: Proof. intros An l Hl ; apply Rseq_cv_shift_compat ; apply Rseq_cv_eq_compat with (Rseq_shift (Rseq_sum An) - Rseq_sum An)%Rseq. clear ; intro p ; unfold Rseq_shift, Rseq_minus ; rewrite Rseq_sum_simpl ; ring. replace 0 with (l - l) by ring ; apply Rseq_cv_minus_compat ; [apply Rseq_cv_shift_compat_reciprocal |] ; assumption. Qed.
imports: Rsequence Rseries_def