proposition: Lemma Rseq_equiv_Rmult_compat : Un ~ Vn -> (r * Un) ~ (r * Vn).
proof: Proof. intros Hu eps Heps. unfold Rseq_mult; unfold Rseq_minus. destruct (Req_dec r 0) as [He|He]. exists 0%nat; intros n Hn. rewrite He; rewrite <- Rmult_minus_distr_l. do 2 rewrite Rabs_mult. change ((IZR 0) n) with (IZR 0); rewrite Rabs_R0. right; field. destruct (Hu eps) as [N HN]; [assumption|]. exists N; intros n Hn. rewrite <- Rmult_minus_distr_l. do 2 rewrite Rabs_mult. rewrite <- Rmult_assoc. pattern (eps * Rabs (r n))%R; rewrite Rmult_comm. rewrite -> Rmult_assoc. apply Rmult_le_compat_l; [apply Rabs_pos|]. apply HN; assumption. Qed.
imports: PeanoNat Reals Setoid Morphisms Rsequence_def Rsequence_base_facts Rsequence_cv_facts Lra