proposition: Lemma Series_minus (a b : nat -> R) : ex_series a -> ex_series b -> Series (fun n => a n - b n) = Series a - Series b.
proof: Proof. intros Ha Hb. rewrite Series_plus => //. rewrite Series_opp => //. apply ex_series_opp in Hb. now simpl in Hb. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Lim_seq Rbar Hierarchy