proposition: Lemma Rseq_big_O_little_O_trans : forall Un Vn Wn, Un = O(Vn) -> Vn = o(Wn) -> Un = o(Wn).
proof: Proof. intros Un Vn Wn HO Ho eps Heps. destruct HO as [M [HM [NO HNO]]]. assert (Hm : Rmax 1 M > 0). eapply Rlt_le_trans; [apply Rlt_0_1|apply RmaxLess1]. destruct (Ho (eps * / Rmax 1 M))%R as [No HNo]. apply Rmult_lt_0_compat; [lra|]. apply Rinv_0_lt_compat; assumption. exists (Nat.max No NO); intros n Hn. eapply Rle_trans. apply HNO; eapply Nat.le_trans; [apply Nat.le_max_r|eexact Hn]. replace eps with ((Rmax 1 M) * eps * / (Rmax 1 M))%R by (field; apply Rgt_not_eq; assumption). do 2 rewrite Rmult_assoc. apply Rmult_le_compat; [apply Rge_le; assumption|apply Rabs_pos|apply RmaxLess2|]. eapply Rle_trans. apply HNo; eapply Nat.le_trans; [apply Nat.le_max_l|eexact Hn]. rewrite Rmult_assoc; apply Rmult_le_compat_r; [|apply Rle_refl]. replace 0%R with (0 * 0)%R by field. apply Rmult_le_compat; try apply Rle_refl. left; apply Rinv_0_lt_compat; assumption. apply Rabs_pos. Qed.
imports: PeanoNat Reals Setoid Morphisms Rsequence_def Rsequence_base_facts Rsequence_cv_facts Lra