proposition: Lemma ex_series_opp (a : nat -> V) : ex_series a -> ex_series (fun n => opp (a n)).
proof: Proof. move => [la Ha]. exists (opp la). exact: is_series_opp. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Lim_seq Rbar Hierarchy