proposition: Lemma Rseq_equiv_cv_neg_infty_compat : Rseq_cv_neg_infty Un -> Rseq_cv_neg_infty Vn.
proof: Proof. intros H M. pose (Mp := Rmin (-1) M). destruct (Heq (/2)%R) as [N HN]; [lra|]. destruct (H (2 * Mp)%R) as [Nm HNm]. exists (Nat.max N Nm); intros n Hn. assert (HMp : Mp < 0). eapply Rle_lt_trans with (-1)%R; [apply Rmin_l|lra]. assert (Hpos : Un n < 0). eapply Rlt_trans with (2 * Mp)%R; [|lra]. apply HNm; eapply Nat.le_trans; [apply Nat.le_max_r|eexact Hn]. assert (Hq : Rabs (Un n - Vn n) <= /2 * Rabs (Un n)). apply HN; eapply Nat.le_trans; [apply Nat.le_max_l|eexact Hn]. assert (Hp : /2 * Rabs (Un n) <= Rabs (Vn n)). replace (/2)%R with (1 + - /2)%R by field. replace (Vn n)%R with (Un n - (Un n - Vn n))%R by field. rewrite Rmult_plus_distr_r; rewrite Rmult_1_l. eapply Rle_trans; [|apply Rabs_triang_inv]. apply Rplus_le_compat_l ; rewrite Ropp_mult_distr_l_reverse. apply Ropp_ge_le_contravar; apply Rle_ge; assumption. assert (Hm : Vn n <= /2 * Un n). unfold Rabs in Hq; repeat destruct Rcase_abs in Hq; try rewrite Ropp_mult_distr_r_reverse in Hq; lra. apply Rlt_le_trans with Mp; [|apply Rmin_r]. apply Rle_lt_trans with (/ 2 * Un n)%R; [assumption|]. apply Rmult_lt_reg_l with 2%R; [lra|]. rewrite <- Rmult_assoc. rewrite Rinv_r; [|apply Rgt_not_eq; lra]. rewrite Rmult_1_l. apply HNm; eapply Nat.le_trans; [apply Nat.le_max_r|eexact Hn]. Qed.
imports: PeanoNat Reals Setoid Morphisms Rsequence_def Rsequence_base_facts Rsequence_cv_facts Lra