proposition: Lemma Rseq_cv_pos_infty_INR : Rseq_cv_pos_infty INR.
proof: Proof. intros M ; pose (n := up (Rabs M)) ; assert (n_pos : (0 <= n)%Z). apply le_0_IZR ; transitivity (Rabs M). apply Rabs_pos. left ; destruct (archimed (Rabs M)) ; assumption. destruct (IZN _ n_pos) as [N HN] ; exists N. intros m m_lb ; apply Rlt_le_trans with (INR N). apply Rle_lt_trans with (Rabs M) ; [apply Rle_abs |]. rewrite INR_IZR_INZ, <- HN ; destruct (archimed (Rabs M)) ; assumption. apply le_INR ; assumption. Qed.
imports: Lia Reals Rsequence_def Rsequence_base_facts Rsequence_cv_facts Rsequence_rel_facts Rsequence_rewrite_facts MyRIneq MyReals Lra