proposition: Lemma is_series_decr_n (a : nat -> V) (n : nat) (l : V) : (0 < n)%nat -> is_series (fun k => a (n + k)%nat) (plus l (opp (sum_n a (pred n)))) -> is_series a l.
proof: Proof. case: n => /= [ | n] Hn Ha. by apply Nat.lt_irrefl in Hn. clear Hn. elim: n a l Ha => [ | n IH] a l Ha. rewrite sum_O in Ha. by apply is_series_decr_1. apply is_series_decr_1. apply IH. replace (plus (plus l (opp (a 0%nat))) (opp (sum_n (fun k : nat => a (S k)) n))) with (plus l (opp (sum_n a (S n)))). by apply Ha. rewrite /sum_n sum_n_m_S sum_Sn_m /=. rewrite <- plus_assoc. apply f_equal. now rewrite opp_plus. by apply Nat.le_0_l. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Lim_seq Rbar Hierarchy