proposition: Lemma Rseq_cv_Rseq_cv_pos_infty_incompat : forall An l, Rseq_cv An l -> Rseq_cv_pos_infty An -> False.
proof: Proof. intros An l Hl Hinfty ; destruct (Hl _ Rlt_0_1) as [M HM] ; destruct (Hinfty (Rabs l + 1)%R) as [N HN] ; apply (Rlt_irrefl (An (Nat.max M N))) ; transitivity (Rabs l + 1)%R. rewrite <- (Rabs_right (An _)). apply Rminus_lt_compat_l_rev, Rle_lt_trans with (R_dist (An (Nat.max M N)) l). apply Rabs_triang_inv. apply HM, Nat.le_max_l. apply Rle_ge ; transitivity (Rabs l + 1)%R. apply Rplus_le_le_0_compat ; [apply Rabs_pos | lra]. left ; apply HN, Nat.le_max_r. apply HN, Nat.le_max_r. Qed.
imports: Lia Rsequence_def Rsequence_base_facts PeanoNat Rinterval MyRIneq Ranalysis_def Lra