proposition: Lemma Rseq_cv_mult_compat : forall Un Vn lu lv, Rseq_cv Un lu -> Rseq_cv Vn lv -> Rseq_cv (Un * Vn) (lu * lv).
proof: Proof. intros Un Vn lu lv Hu Hv eps Heps. destruct (Rseq_cv_bound Un lu) as [Mb [HMb Hb]]; [assumption|]. pose (eps1 := (eps / 2 / (Rmax 1 (Rabs lv)))%R). pose (eps2 := (eps / 2 / Mb)%R). assert (Heps1 : eps1 > 0). unfold eps1; repeat apply Rmult_gt_0_compat; try lra. apply Rinv_0_lt_compat; eapply Rlt_le_trans; [apply Rlt_0_1|apply RmaxLess1]. assert (Heps2 : eps2 > 0). unfold eps2; repeat apply Rmult_gt_0_compat; try lra. apply Rinv_0_lt_compat; assumption. destruct (Hu eps1) as [Nu HNu]; [assumption|]. destruct (Hv eps2) as [Nv HNv]; [assumption|]. exists (Nat.max Nu Nv); intros n Hn. unfold R_dist; unfold Rseq_mult. replace (Un n * Vn n - lu * lv)%R with ((Un n * Vn n - Un n * lv) + (Un n * lv - lu * lv))%R by field. eapply Rle_lt_trans; [apply Rabs_triang|]. replace eps with (eps / 2 + eps / 2)%R by field. apply Rplus_lt_compat. rewrite <- Rmult_minus_distr_l; rewrite Rabs_mult. eapply Rle_lt_trans. apply Rmult_le_compat_r; [apply Rabs_pos|]. apply Hb. replace (eps / 2)%R with (Mb * (eps / 2 / Mb))%R by (field; apply Rgt_not_eq; assumption). apply Rmult_lt_compat_l; [assumption|]. apply HNv; eapply Nat.le_trans; [apply Nat.le_max_r|eexact Hn]. unfold Rminus; rewrite <- Ropp_mult_distr_l_reverse. rewrite <- Rmult_plus_distr_r. rewrite Rabs_mult. destruct (Req_dec lv 0) as [Hlv|Hlv]. rewrite Hlv; rewrite Rabs_R0; rewrite Rmult_0_r; lra. eapply Rlt_le_trans. apply Rmult_lt_compat_r; [apply Rabs_pos_lt; assumption|]. apply HNu; eapply Nat.le_trans; [apply Nat.le_max_l|eexact Hn]. unfold eps1. unfold Rdiv; rewrite Rmult_assoc; rewrite <- Rmult_1_r. apply Rmult_le_compat_l; [lra|]. assert (Hmax : Rmax 1 (Rabs lv) > 0). eapply Rlt_le_trans with 1; [lra|apply RmaxLess1]. pattern 1 at 2; rewrite <- (Rinv_l (Rmax 1 (Rabs lv))). apply Rmult_le_compat_l. left; apply Rinv_0_lt_compat; assumption. apply RmaxLess2. apply Rgt_not_eq; assumption. Qed.
imports: Lia Rsequence_def Rsequence_base_facts PeanoNat Rinterval MyRIneq Ranalysis_def Lra