proposition: Lemma Rseq_equiv_opp_compat : Un ~ Vn -> (- Un) ~ (- Vn).
proof: Proof. intros Hu eps Heps. destruct (Hu eps) as [N HN]; [assumption|]. exists N; intros n Hn. unfold Rseq_minus; unfold Rseq_opp. unfold Rminus; rewrite <- Ropp_plus_distr. repeat rewrite Rabs_Ropp. apply HN; assumption. Qed.
imports: PeanoNat Reals Setoid Morphisms Rsequence_def Rsequence_base_facts Rsequence_cv_facts Lra