proposition: Lemma Rseq_equiv_cv_pos_infty_compat : Rseq_cv_pos_infty Un -> Rseq_cv_pos_infty Vn.
proof: Proof. intros H M. pose (Mp := Rmax 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 : 0 < Mp). eapply Rlt_le_trans with 1%R; [lra|apply RmaxLess1]. assert (Hpos : 0 < Un n). eapply Rlt_trans with (2 * Mp)%R. apply Rmult_gt_0_compat; [lra|assumption]. 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; lra. apply Rle_lt_trans with Mp; [apply RmaxLess2|]. apply Rlt_le_trans with (/ 2 * Un n)%R. 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]. apply Rge_le; assumption. Qed.
imports: PeanoNat Reals Setoid Morphisms Rsequence_def Rsequence_base_facts Rsequence_cv_facts Lra