proposition: Lemma Rseq_big_O_trans : forall Un Vn Wn, Un = O(Vn) -> Vn = O(Wn) -> Un = O(Wn).
proof: Proof. intros Un Vn Wn Hu Hv. destruct Hu as [Mu [HMu Hu]]; destruct Hv as [Mv [HMv Hv]]. exists (Mu * Mv)%R; split. replace 0 with (0 * 0)%R by field. apply Rmult_ge_compat; (assumption || apply Rge_refl). destruct Hu as [Nu Hu]; destruct Hv as [Nv Hv]. exists (Nat.max Nu Nv); intros n Hn. apply Rle_trans with (r2 := (Mu * Rabs (Vn n))%R). apply (Hu n); eapply Nat.le_trans; [apply Nat.le_max_l|eexact Hn]. rewrite Rmult_assoc. apply Rmult_le_compat_l. apply Rge_le; assumption. 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