proposition: Lemma CV_radius_ext (a b : nat -> R) : (forall n, a n = b n) -> CV_radius a = CV_radius b.
proof: Proof. move => Heq. rewrite /CV_radius /Lub_Rbar. case: ex_lub_Rbar => la [ub_a lub_a] ; case: ex_lub_Rbar => lb [ub_b lub_b] /=. apply Rbar_le_antisym. apply lub_a => x Hx. apply ub_b ; move: Hx. apply ex_series_ext => n ; by rewrite Heq. apply lub_b => x Hx. apply ub_a ; move: Hx. apply ex_series_ext => n ; by rewrite Heq. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Lub Hierarchy Continuity Derive Seq_fct Series