proposition: Lemma Rseq_little_O_trans : forall Un Vn Wn, Un = o(Vn) -> Vn = o(Wn) -> Un = o(Wn).
proof: Proof. intros Un Vn Wn Hu Hv eps Heps. destruct (Hu 1) as [Nu HNu]; [lra|]. destruct (Hv eps) as [Nv Hnv]; [assumption|]. exists (Nat.max Nu Nv). intros n Hn. apply Rle_trans with (r2 := (Rabs (Vn n))%R). rewrite <- Rmult_1_l; 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