proposition: Lemma CV_radius_opp (a : nat -> R) : (CV_radius (PS_opp a)) = (CV_radius a).
proof: Proof. rewrite -(CV_radius_scal (-1)). apply CV_radius_ext => n. by rewrite /PS_scal /PS_opp scal_opp_l scal_opp_r opp_opp scal_one. rewrite -Ropp_0 ; apply Rlt_not_eq, Ropp_lt_contravar, Rlt_0_1. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Lub Hierarchy Continuity Derive Seq_fct Series