proposition: Lemma Rseq_little_O_big_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 Hv as [M [HM [NO HNO]]]. destruct (Hu (eps * / Rmax 1 M)%R) as [No HNo]. apply Rmult_gt_0_compat; [lra|]. apply Rinv_0_lt_compat; eapply Rlt_le_trans; [apply Rlt_0_1|apply RmaxLess1]. exists (Nat.max NO No); intros n Hn. eapply Rle_trans. apply HNo; eapply Nat.le_trans; [apply Nat.le_max_r|eexact Hn]. rewrite Rmult_assoc. apply Rmult_le_compat_l; [lra|]. eapply Rle_trans. apply Rmult_le_compat_l. left; apply Rinv_0_lt_compat. eapply Rlt_le_trans; [apply Rlt_0_1|apply RmaxLess1]. apply HNO; eapply Nat.le_trans; [apply Nat.le_max_l|eexact Hn]. rewrite <- Rmult_assoc. rewrite <- Rmult_1_l; apply Rmult_le_compat_r; [apply Rabs_pos|]. pattern 1 at 2; rewrite <- (Rinv_l (Rmax 1 M)). apply Rmult_le_compat_l. left; apply Rinv_0_lt_compat; eapply Rlt_le_trans; [apply Rlt_0_1|apply RmaxLess1]. apply RmaxLess2. apply Rgt_not_eq. eapply Rlt_le_trans; [apply Rlt_0_1|apply RmaxLess1]. Qed.
imports: PeanoNat Reals Setoid Morphisms Rsequence_def Rsequence_base_facts Rsequence_cv_facts Lra