proposition: Lemma Rseq_little_O_Rmult_compat_l : Un = o(Vn) -> (r * Un) = o(Vn).
proof: Proof. intros Hu eps Heps. destruct (Req_dec r 0) as [He|He]. exists 0%nat; intros n Hn. unfold Rseq_mult; rewrite He. rewrite Rmult_0_l; rewrite Rabs_R0. rewrite <- (Rmult_0_l 0). apply Rmult_le_compat; (apply Rle_refl || lra || apply Rabs_pos). destruct (Hu (eps * / Rabs r)%R) as [N HN]. apply Rmult_gt_0_compat; [|apply Rinv_0_lt_compat; apply Rabs_pos_lt]; assumption. exists N; intros n Hn. unfold Rseq_mult; rewrite Rabs_mult. eapply Rle_trans. apply Rmult_le_compat_l; [apply Rabs_pos|]. apply HN; assumption. change (r n) with r. right; field; apply Rabs_no_R0; assumption. Qed.
imports: PeanoNat Reals Setoid Morphisms Rsequence_def Rsequence_base_facts Rsequence_cv_facts Lra