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