proposition: Lemma Rseq_big_O_Rmult_compat_l : Un = O(Vn) -> (r * Un) = O(Vn).
proof: Proof. intros Hu. destruct Hu as [M [HM [N HN]]]. exists (Rabs r * M)%R; split. rewrite <- (Rmult_0_l 0). apply Rmult_ge_compat; apply Rle_refl || (apply Rle_ge; apply Rabs_pos) || assumption. exists N; intros n Hn. unfold Rseq_mult. rewrite Rabs_mult; 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