proposition: Lemma is_pseries_minus (a b : nat -> V) (x:K) (la lb : V) : is_pseries a x la -> is_pseries b x lb -> is_pseries (PS_minus a b) x (plus la (opp lb)).
proof: Proof. move => Ha Hb. apply is_pseries_plus. exact: Ha. by apply is_pseries_opp. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Lub Hierarchy Continuity Derive Seq_fct Series