proposition: Lemma Rseq_big_O_opp_compat_r : Un = O(Vn) -> Un = O(- Vn).
proof: Proof. intros H. destruct H as [M [HM [N H]]]. exists M; split; [exact HM|]. exists N; intros n Hn. unfold Rseq_opp; rewrite Rabs_Ropp. apply (H n); apply Hn. Qed.
imports: PeanoNat Reals Setoid Morphisms Rsequence_def Rsequence_base_facts Rsequence_cv_facts Lra