proposition: Lemma ex_pseries_opp (a : nat -> V) (x : K) : ex_pseries a x -> ex_pseries (PS_opp a) x.
proof: Proof. intros [l Hl]. exists (opp l). now apply is_pseries_opp. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Lub Hierarchy Continuity Derive Seq_fct Series