proposition: Lemma Rser_cv_reorder : forall n Un l, Rser_cv Un l -> Rser_cv (fun k => Un (k - S n)%nat) (l + INR (S n) * (Un O)).
proof: Proof. intros n Un l Uncv. intros eps Heps. destruct (Uncv eps Heps) as (N, Hn). exists (S n + N)%nat. intros k Hk. assert (HkN : (k >= N)%nat) by intuition. generalize (Hn k HkN) ; intros Hcv. unfold R_dist in *. assert (forall k n, (k >= S n)%nat -> sum_f_R0 (fun k0 : nat => Un (k0 - S n)%nat) k = sum_f_R0 Un (k - S n) + INR (S n) * Un O). intros m n0 Hmn0. induction Hmn0. induction n0. simpl. ring. rewrite sum_reorder_0. repeat rewrite S_INR. rewrite Nat.sub_diag. simpl. ring. intuition. rewrite tech5. rewrite IHHmn0. rewrite Nat.sub_succ_l. rewrite tech5. ring. intuition. rewrite H. ring_simplify (sum_f_R0 Un (k - S n) + INR (S n) * Un 0%nat - (l + INR (S n) * Un 0%nat)). assert (k - S n >= N)%nat by intuition. generalize (Hn (k - S n)%nat H0). intuition. intuition. 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