proposition: Lemma CV_opp : forall (An:nat -> R) (l:R), Un_cv An l -> Un_cv (opp_seq An) (- l).
proof: Proof. intros An l. unfold Un_cv; unfold Rdist; intros. elim (H eps H0); intros. exists x; intros. unfold opp_seq; replace (- An n - - l) with (- (An n - l)); [ rewrite Rabs_Ropp | ring ]. apply H1; assumption. Qed.
imports: Rbase Rfunctions Rseries Lia