proposition: Lemma is_pseries_ext (a b : nat -> V) (x : K) (l:V) : (forall n, a n = b n) -> (is_pseries a x l) -> is_pseries b x l.
proof: Proof. move => Heq Ha. apply is_series_ext with (2 := Ha). move => n. by rewrite Heq. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Lub Hierarchy Continuity Derive Seq_fct Series