proposition: Lemma Rseq_equiv_big_O_incl : forall Un Vn, Un ~ Vn -> Un = O(Vn).
proof: Proof. intros Un Vn H. apply Rseq_equiv_sym in H. destruct (H 1) as [N HN]; [lra|]. exists 2; split; [lra|]. exists N; intros n Hn. replace (Un n) with (Un n - Vn n + Vn n)%R by field. eapply Rle_trans; [apply Rabs_triang|]. change 2 with (1 + 1)%R. rewrite Rmult_plus_distr_r. apply Rplus_le_compat; [|rewrite Rmult_1_l; apply Rle_refl]. rewrite Rabs_minus_sym; apply HN; assumption. Qed.
imports: PeanoNat Reals Setoid Morphisms Rsequence_def Rsequence_base_facts Rsequence_cv_facts Lra