proposition: Lemma ex_pseries_minus (a b : nat -> V) (x : K) : ex_pseries a x -> ex_pseries b x -> ex_pseries (PS_minus a b) x.
proof: Proof. move => Ha Hb. apply ex_pseries_plus. exact: Ha. by apply ex_pseries_opp. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Lub Hierarchy Continuity Derive Seq_fct Series