proposition: Lemma Rser_Rser_rem_lt_le : forall Un Vn x l (H : Rser_cv Vn l) n, (forall k, (k > n)%nat -> Vn k <= Un (k - S n)%nat) -> {k | (k > n)%nat /\ Vn k < Un (k - S n)%nat} -> Rser_cv Un x -> Rser_rem Vn l H n < x.
proof: Proof. intros Un Vn x l Hv n Hle Hlt Hu. destruct (seq_exist_subproof Un Vn n Hle Hlt) as (Wn, [k2 [Hwn11 [Hwn2 Hwn3]]]). assert (Hwn : Rser_cv Wn (x + INR (S n) * (Un O) - l)). assert (H1 : Rser_cv (fun k => Un (k - S n)%nat) (x + INR (S n) * (Un O))). apply Rser_cv_reorder. assumption. apply Rser_cv_ext with ((fun k => Un (k - S n)%nat) - Vn)%Rseq. intros k. generalize (Hwn11 k) ; intros Hwn1. destruct Hwn1 as (Hwn1, _). unfold Rseq_minus. rewrite <- Hwn1. ring. apply Rser_cv_minus_compat ; intuition. pose (l1 := x + INR (S n) * Un 0%nat - l). assert (H1 : Rser_cv (Vn + Wn)%Rseq (l + l1)). apply Rser_cv_plus_compat ; assumption. rewrite (Rser_Rser_rem_equiv Un (Vn + Wn)%Rseq x (l + l1) H1 n). apply Rser_rem_lt_le. unfold Rseq_plus. intuition. replace (Vn k) with (Vn k + 0) by intuition. apply Rplus_le_compat. intuition. destruct (Hwn11 k) as (_, Hwn1). destruct (Hwn1 H) ; intuition. destruct Hlt as (k, H2). exists k ; intuition. destruct (Hwn11 k) as (Hwn1, Hwn5). unfold Rseq_plus. rewrite Hwn1. intuition. intros k. destruct (Hwn11 (S n + k)%nat) as (Hwn1, Hwn5). unfold Rseq_shifts, Rseq_plus. rewrite Hwn1. intuition. assumption. Qed.
imports: Reals Rsequence Rseries_def Rseries_base_facts Rseries_pos_facts Rseries_remainder_facts Rseries_cv_facts Rseries_usual Lra PeanoNat Rtactic MyRIneq Rsequence