proposition: Lemma Rseq_big_O_mult_compat : Un = O(Wn) -> Vn = O(Xn) -> (Un * Vn) = O(Wn * Xn).
proof: Proof. intros Hu Hv. destruct Hu as [Mu [HMu [Nu Hu]]]. destruct Hv as [Mv [HMv [Nv Hv]]]. exists (Mu * Mv)%R; split. replace 0 with (0 * 0)%R by field. apply Rmult_ge_compat; auto with real. exists (Nat.max Nu Nv). intros n Hn. unfold Rseq_mult. do 2 (rewrite Rabs_mult). replace (Mu * Mv * (Rabs (Wn n) * Rabs (Xn n)))%R with ((Mu * Rabs (Wn n)) * (Mv * Rabs (Xn n)))%R by field. apply Rmult_le_compat; try (apply Rabs_pos). apply (Hu n); eapply Nat.le_trans; [apply Nat.le_max_l|eexact Hn]. apply (Hv n); eapply Nat.le_trans; [apply Nat.le_max_r|eexact Hn]. Qed.
imports: PeanoNat Reals Setoid Morphisms Rsequence_def Rsequence_base_facts Rsequence_cv_facts Lra