proposition: Lemma is_series_decr_1 (a : nat -> V) (l : V) : is_series (fun k => a (S k)%nat) (plus l (opp (a O))) -> is_series a l.
proof: Proof. intros H. apply filterlim_ext_loc with (fun v => plus (a 0%nat) (sum_n (fun k : nat => a (S k)) (pred v))). exists 1%nat. intros n Hn; apply sym_eq. rewrite /sum_n sum_Sn_m. apply f_equal. rewrite sum_n_m_S. apply f_equal ; lia. by apply Nat.le_0_l. replace l with (plus (a 0%nat) (plus l (opp (a 0%nat)))). apply filterlim_comp_2 with (3 := filterlim_plus _ _). apply filterlim_id. apply filterlim_const. apply filterlim_comp with (f:= fun x => pred x) (2:=H). intros P (N1,HN1). exists (S N1). intros n Hn; apply HN1; lia. rewrite plus_comm; rewrite <- plus_assoc. rewrite (plus_comm _ (a 0%nat)); rewrite plus_opp_r. apply plus_zero_r. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Lim_seq Rbar Hierarchy