proposition: Lemma Rseq_cv_opp_compat : forall Un lu, Rseq_cv Un lu -> Rseq_cv (- Un) (- lu).
proof: Proof. intros Un lu Hu eps Heps. destruct (Hu eps) as [Nu HNu]; [assumption|]. exists Nu; intros n Hn. unfold R_dist; unfold Rseq_opp. replace (- Un n - - lu)%R with (- (Un n - lu))%R by field. rewrite Rabs_Ropp. apply HNu; exact Hn. Qed.
imports: Lia Rsequence_def Rsequence_base_facts PeanoNat Rinterval MyRIneq Ranalysis_def Lra