proposition: Lemma Rseq_cv_abs_pos_infty : Rseq_cv_pos_infty Un -> Rseq_cv_pos_infty (|Un|).
proof: Proof. intros HU M. destruct (HU (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). apply (HN _ Hn). apply RRle_abs. Qed.
imports: Lia Rsequence_def Rsequence_base_facts PeanoNat Rinterval MyRIneq Ranalysis_def Lra