proposition: Lemma ex_series_incr_n (a : nat -> V) (n : nat) : ex_series a <-> ex_series (fun k => a (n + k)%nat).
proof: Proof. case: n => [ | n]. split ; apply ex_series_ext ; by intuition. split ; move => [la Ha]. exists (plus la (opp (sum_n a (pred (S n))))). apply is_series_incr_n. by apply Nat.lt_0_succ. now rewrite -plus_assoc plus_opp_l plus_zero_r. exists (plus la (sum_n a (pred (S n)))). apply is_series_decr_n with (S n). by apply Nat.lt_0_succ. now rewrite -plus_assoc plus_opp_r plus_zero_r. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Lim_seq Rbar Hierarchy