proposition: Lemma Rseq_cv_finite_pos_mult_neg_infty_l : forall l, 0 < l -> Rseq_cv Un l -> Rseq_cv_neg_infty Vn -> Rseq_cv_neg_infty (Vn * Un).
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 Rlt_le_trans with ((l*/2)*(-(Rabs M)*(2*/l)))%R. replace ((Vn * Un)%Rseq n) with (Vn n * Un n)%R by reflexivity. rewrite (Rmult_comm (Vn n) (Un n)). apply Ropp_lt_cancel. rewrite <- (Ropp_mult_distr_r_reverse (Un n) (Vn n)). rewrite <- Ropp_mult_distr_r_reverse, <- Ropp_mult_distr_l_reverse, Ropp_involutive. replace (- (l * /2 * (- Rabs M * (2 * /l))))%R with (l * /2 * (Rabs M * (2 * /l)))%R by ring. apply Rmult_le_0_lt_compat. repeat apply Rmult_gt_0_compat; try lra. replace 0%R with (Rabs M * 0)%R by field. apply Rmult_le_compat_l. apply Rabs_pos. apply Rlt_le. repeat apply Rmult_gt_0_compat; try lra. apply Rinv_0_lt_compat. exact Hl. replace (l * /2)%R with (l - (l * /2))%R by field. apply Rminus_lt. unfold Rminus. rewrite Rplus_comm, <- Rplus_assoc, Rplus_comm. replace 0 with (- (l * /2) + (l * /2))%R by ring. apply Rplus_lt_compat_l. apply Rle_lt_trans with (Rabs (Un n+ - l)). rewrite <- Rabs_Ropp, Ropp_plus_distr, Ropp_involutive. apply RRle_abs. apply HN; lia. apply Ropp_lt_cancel. rewrite (Rmult_comm 2 (/l)), <- Ropp_mult_distr_l_reverse, Ropp_involutive. apply HN0; lia. replace (l * /2 * (- Rabs M *(2 * /l)))%R with (- Rabs M)%R. rewrite <- (Ropp_involutive M). apply Ropp_ge_le_contravar. rewrite Rabs_Ropp. apply Rle_ge. apply RRle_abs. field. apply Rgt_not_eq. exact Hl. Qed.
imports: Lia Rsequence_def Rsequence_base_facts PeanoNat Rinterval MyRIneq Ranalysis_def Lra