proposition: Lemma Rseq_cv_not_infty : forall (Un : nat -> R), ~ ((exists l, Rseq_cv Un l) /\ Rseq_cv_pos_infty Un).
proof: Proof. intros Un Hf. destruct Hf as [[l Hl] Hinf]. unfold Rseq_cv in Hl. unfold Rseq_cv_pos_infty in Hinf. destruct (Hinf (l+1)%R) as [ N HN]. destruct (Hl 1) as [N0 HN0]. auto with *. apply Rlt_irrefl with (Un (Nat.max N N0)). apply Rlt_trans with (l+1)%R. replace (Un (Nat.max N N0)) with (l+(Un (Nat.max N N0)-l))%R by ring. apply Rplus_lt_compat_l. apply Rle_lt_trans with (Rabs (Un (Nat.max N N0) - l)). apply RRle_abs. apply HN0. apply Nat.le_max_r. apply HN. apply Nat.le_max_l. Qed.
imports: Lia Reals Rsequence_def Rsequence_base_facts Rsequence_cv_facts Rsequence_rel_facts Rsequence_usual_facts Lra