proposition: Lemma Rseq_little_O_Rmult_compat_r : Un = o(Vn) -> r <> 0 -> Un = o(r * Vn).
proof: Proof. intros Hu Hr eps Heps. destruct (Hu (eps * Rabs r)%R) as [N HN]. apply Rmult_gt_0_compat; [|apply Rabs_pos_lt]; assumption. exists N; intros n Hn. unfold Rseq_mult; rewrite Rabs_mult. rewrite <- Rmult_assoc. apply HN; assumption. Qed.
imports: PeanoNat Reals Setoid Morphisms Rsequence_def Rsequence_base_facts Rsequence_cv_facts Lra