proposition: Lemma Rseq_big_O_Rmult_compat_r : Un = O(Vn) -> r <> 0 -> Un = O(r * Vn).
proof: Proof. intros Hu Hr. 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 || assumption || idtac. left; apply Rinv_0_lt_compat; apply Rabs_pos_lt; assumption. exists N; intros n Hn. unfold Rseq_mult; rewrite Rabs_mult. change (r n) with r. field_simplify; [|apply Rabs_no_R0; assumption]. unfold Rdiv; repeat rewrite Rinv_1; repeat rewrite Rmult_1_r. apply HN; assumption. Qed.
imports: PeanoNat Reals Setoid Morphisms Rsequence_def Rsequence_base_facts Rsequence_cv_facts Lra