proposition: Lemma PSeries_minus (a b : nat -> R) (x : R) : ex_pseries a x -> ex_pseries b x -> PSeries (PS_minus a b) x = PSeries a x - PSeries b x.
proof: Proof. move => Ha Hb. rewrite PSeries_plus. by rewrite PSeries_opp. exact: Ha. by apply ex_pseries_opp. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Lub Hierarchy Continuity Derive Seq_fct Series