proposition: Lemma Rseq_little_O_big_O_incl : forall Un Vn, Un = o(Vn) -> Un = O(Vn).
proof: Proof. intros Un Vn H. destruct (H 1) as [N HN]; [lra|]. exists 1; split; [lra|]. exists N; intros n Hn. apply HN; assumption. Qed.
imports: PeanoNat Reals Setoid Morphisms Rsequence_def Rsequence_base_facts Rsequence_cv_facts Lra