proposition: Lemma Rseq_cv_finite_pos_mult_pos_infty_l : forall l, 0 < l -> Rseq_cv Un l -> Rseq_cv_pos_infty Vn -> Rseq_cv_pos_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 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 Rgt_not_eq. exact Hl. replace ((Vn * Un)%Rseq n) with (Vn n * Un n)%R by reflexivity. rewrite (Rmult_comm (Vn n) (Un n)). 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. rewrite <- Rplus_assoc. rewrite 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. rewrite Ropp_plus_distr. rewrite Ropp_involutive. apply RRle_abs. apply HN; lia. rewrite (Rmult_comm 2 (/l)). apply HN0; lia. Qed.
imports: Lia Rsequence_def Rsequence_base_facts PeanoNat Rinterval MyRIneq Ranalysis_def Lra