proposition: Lemma Rser_cv_shift_reciprocal : forall Un l, Rser_cv (Rseq_shift Un) (l - (Un O)) -> Rser_cv Un l.
proof: Proof. intros Un l H. assert (EC : forall (a:Rseq) (b x:R), Rseq_cv (a - b)%Rseq (x - b) -> Rseq_cv a x). intros; apply Rseq_cv_eq_compat with (a - b + b)%Rseq. intro; compute; field. replace x with (x - b + b) by field. apply Rseq_cv_plus_compat. assumption. apply Rseq_constant_cv. eapply EC with (Un O). apply Rseq_cv_shift_compat. apply Rseq_cv_eq_compat with (sum_f_R0 (Rseq_shift Un)). symmetry ; apply Rsum_shift. apply H. Qed.
imports: Rsequence Rseries_def Rseries_base_facts Rseries_pos_facts MyNat MyRIneq PeanoNat Lra Rtactic