proposition: Lemma Rseq_little_O_opp_compat_r : Un = o(Vn) -> Un = o(- Vn).
proof: Proof. intros H eps Heps. destruct (H eps) as [N HN]; [assumption|]. exists N; intros n Hn. unfold Rseq_opp. rewrite Rabs_Ropp. apply HN; assumption. Qed.
imports: PeanoNat Reals Setoid Morphisms Rsequence_def Rsequence_base_facts Rsequence_cv_facts Lra