1 files changed, 23 insertions, 0 deletions
diff --git a/theories/Reals/Rseries.v b/theories/Reals/Rseries.v
index 57b9d3d2f..b3e297598 100644
--- a/theories/Reals/Rseries.v
+++ b/theories/Reals/Rseries.v
@@ -404,3 +404,26 @@ Proof.
   apply Rinv_neq_0_compat.
   assumption.
 Qed.
+
+(* Convergence is preserved after shifting the indices. *)
+Lemma CV_shift : 
+  forall f k l, Un_cv (fun n => f (n + k)%nat) l -> Un_cv f l.
+intros f' k l cvfk eps ep; destruct (cvfk eps ep) as [N Pn].
+exists (N + k)%nat; intros n nN; assert (tmp: (n = (n - k) + k)%nat).
+ rewrite Nat.sub_add;[ | apply le_trans with (N + k)%nat]; auto with arith.
+rewrite tmp; apply Pn; apply Nat.le_add_le_sub_r; assumption.
+Qed.
+
+Lemma CV_shift' : 
+  forall f k l, Un_cv f l -> Un_cv (fun n => f (n + k)%nat) l.
+intros f' k l cvf eps ep; destruct (cvf eps ep) as [N Pn].
+exists N; intros n nN; apply Pn; auto with arith.
+Qed.
+
+(* Growing property is preserved after shifting the indices (one way only) *)
+
+Lemma Un_growing_shift : 
+   forall k un, Un_growing un -> Un_growing (fun n => un (n + k)%nat).
+Proof.
+intros k un P n; apply P.
+Qed.