proposition: Lemma Rseq_cv_abs_neg_infty : Rseq_cv_neg_infty Un -> Rseq_cv_pos_infty (|Un|).
proof: Proof. intros HU M. assert (H : Rseq_cv_pos_infty (-Un)). apply Rseq_cv_neg_infty_opp_compat. apply HU. destruct (H (Rabs M)) as [N HN]. exists N. intros n Hn. apply Rle_lt_trans with (Rabs M). apply RRle_abs. apply Rlt_le_trans with (- (Un n))%R. apply (HN _ Hn). unfold Rseq_abs. rewrite <- Rabs_Ropp. apply RRle_abs. Qed.
imports: Lia Rsequence_def Rsequence_base_facts PeanoNat Rinterval MyRIneq Ranalysis_def Lra