proposition: Lemma ex_series_incr_1 (a : nat -> V) : ex_series a <-> ex_series (fun k => a (S k)%nat).
proof: Proof. split ; move => [la Ha]. exists (plus la (opp (a O))). apply is_series_incr_1. now rewrite -plus_assoc plus_opp_l plus_zero_r. exists (plus la (a O)). apply is_series_decr_1. now rewrite -plus_assoc plus_opp_r plus_zero_r. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Lim_seq Rbar Hierarchy