proposition: Lemma Rseq_cv_finite_neg_mult_neg_infty_r : forall l, l < 0 -> Rseq_cv Un l -> Rseq_cv_neg_infty Vn -> Rseq_cv_pos_infty (Un * Vn).
proof: Proof. intros l Hl Hu Hv M. destruct (Hu (-(l*/2))%R) as [N HN]. repeat apply Rmult_gt_0_compat; try lra. destruct (Hv ((Rabs M)*(/l*2))%R) as [N0 HN0]. exists (N+N0)%nat; intros n Hn. apply Rle_lt_trans with (-(l*/2)*(-(Rabs M)*(2*/l)))%R. replace (-(l*/2)*(-(Rabs M)*(2*/l)))%R with (Rabs M). apply RRle_abs. field. apply Rlt_not_eq. exact Hl. replace ((Un * Vn)%Rseq n) with (Un n * Vn n)%R by reflexivity. replace (Un n * Vn n)%R with ((- Un n) * (- Vn n))%R by ring. apply Rmult_le_0_lt_compat. repeat apply Rmult_gt_0_compat; try lra. replace (-(Rabs M)*(2*/l))%R with ((Rabs M)*(- 2*/l))%R by ring. replace 0%R with (Rabs M * 0)%R by field. apply Rmult_le_compat_l. apply Rabs_pos. apply Rlt_le. change (IZR (-2)) with (- (IZR 2))%R. rewrite Ropp_mult_distr_l_reverse, <- Ropp_mult_distr_r_reverse. repeat apply Rmult_gt_0_compat; try lra. apply Ropp_0_gt_lt_contravar. apply Rinv_lt_0_compat. exact Hl. apply Ropp_lt_contravar. replace (l * /2)%R with (l - (l * /2))%R by field. apply Rminus_lt. unfold Rminus. rewrite Ropp_plus_distr, Ropp_involutive, <- Rplus_assoc. replace 0 with (- (l * /2) + (l * /2))%R by ring. apply Rplus_lt_compat_r. apply Rle_lt_trans with (Rabs (Un n+ - l)). apply RRle_abs. apply HN; lia. rewrite Ropp_mult_distr_l_reverse. apply Ropp_gt_lt_contravar. apply Rlt_gt. rewrite (Rmult_comm 2 (/l)). apply HN0; lia. Qed.
imports: Lia Rsequence_def Rsequence_base_facts PeanoNat Rinterval MyRIneq Ranalysis_def Lra