proposition: Lemma Rseq_equiv_mult_compat : Un ~ Wn -> Vn ~ Xn -> (Un * Vn) ~ (Wn * Xn).
proof: Proof. intros Hu Hv eps Heps. pose (eps1 := (eps / 2)%R). pose (eps2 := (eps / (eps + 2))%R). assert (Heps1 : eps1 > 0). unfold eps1; lra. assert (Heps2 : eps2 > 0). unfold eps2; unfold Rdiv. apply Rmult_gt_0_compat; [assumption|]. apply Rinv_0_lt_compat; lra. destruct (Hu eps1) as [Nu HNu]; [assumption|]. destruct (Hv eps2) as [Nv HNv]; [assumption|]. exists (Nat.max Nu Nv); intros n Hn. unfold Rseq_minus; unfold Rseq_mult. replace (Un n * Vn n - Wn n * Xn n)%R with ((Un n * Vn n - Wn n * Vn n) + (Wn n * Vn n - Wn n * Xn n))%R by ring. replace (eps * Rabs (Un n * Vn n))%R with (eps / 2 * Rabs (Un n * Vn n) + eps / 2 * Rabs (Un n * Vn n))%R by field. eapply Rle_trans; [apply Rabs_triang|]. apply Rplus_le_compat. replace (Un n * Vn n - Wn n * Vn n)%R with ((Un n - Wn n) * Vn n)%R by ring. repeat rewrite Rabs_mult; rewrite <- Rmult_assoc. apply Rmult_le_compat_r; [apply Rabs_pos|]. apply HNu; eapply Nat.le_trans; [apply Nat.le_max_l|eexact Hn]. replace (Wn n * Vn n - Wn n * Xn n)%R with (Wn n * (Vn n - Xn n))%R by field. repeat rewrite Rabs_mult. replace (eps / 2)%R with (eps2 * (eps1 + 1))%R by (unfold eps1; unfold eps2; field; apply Rgt_not_eq; lra). replace (eps2 * (eps1 + 1) * (Rabs (Un n) * Rabs (Vn n)))%R with ((eps1 * Rabs (Un n) + Rabs (Un n)) * ((eps2 * Rabs (Vn n))))%R by field. apply Rmult_le_compat; try apply Rabs_pos. replace (Wn n) with ((Wn n - Un n) + Un n)%R by field. eapply Rle_trans; [apply Rabs_triang|]. apply Rplus_le_compat_r; rewrite Rabs_minus_sym. apply HNu; eapply Nat.le_trans; [apply Nat.le_max_l|eexact Hn]. apply HNv; eapply Nat.le_trans; [apply Nat.le_max_r|eexact Hn]. Qed.
imports: PeanoNat Reals Setoid Morphisms Rsequence_def Rsequence_base_facts Rsequence_cv_facts Lra