proposition: Lemma Rseq_little_O_mult_compat : Un = o(Wn) -> Vn = o(Xn) -> (Un * Vn) = o(Wn * Xn).
proof: Proof. intros Hu Hv eps Heps. destruct (Hu (sqrt eps)) as [Nu HNu]; [apply sqrt_lt_R0; assumption|]. destruct (Hv (sqrt eps)) as [Nv HNv]; [apply sqrt_lt_R0; assumption|]. exists (Nat.max Nu Nv); intros n Hn. unfold Rseq_mult. repeat rewrite Rabs_mult. rewrite <- (sqrt_def eps); [|left; assumption]. replace (sqrt eps * sqrt eps * (Rabs (Wn n) * Rabs (Xn n)))%R with ((sqrt eps * Rabs (Wn n)) * (sqrt eps * Rabs (Xn n)))%R by field. apply Rmult_le_compat; try apply Rabs_pos. apply (HNu n); eapply Nat.le_trans; [apply Nat.le_max_l|eexact Hn]. apply (HNv 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