proposition: Lemma is_series_incr_1 (a : nat -> V) (l : V) : is_series a (plus l (a O)) -> is_series (fun k => a (S k)%nat) l.
proof: Proof. intros H. apply filterlim_ext with (fun k => plus (sum_n a (S k)) (opp (a 0%nat))). induction x; simpl. rewrite sum_Sn !sum_O (plus_comm _ (a 1%nat)); rewrite <- plus_assoc. now rewrite plus_opp_r plus_zero_r. rewrite !sum_Sn -IHx -!sum_Sn sum_Sn; simpl. rewrite <- plus_assoc, <- (plus_assoc _ _ (a (S (S x)))). apply f_equal; apply plus_comm. apply filterlim_comp with (G:=(locally (plus l (a 0%nat)))) (g:=fun x => plus x (opp (a 0%nat))). apply filterlim_comp with (f:= fun x => S x) (2:=H). apply eventually_subseq; intros n; lia. pattern l at 2; replace l with (plus (plus l (a 0%nat)) (opp (a 0%nat))). apply filterlim_comp_2 with (3 := filterlim_plus _ _). apply filterlim_id. apply filterlim_const. rewrite -plus_assoc plus_opp_r. apply plus_zero_r. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Lim_seq Rbar Hierarchy