proposition: Lemma Rpser_opp_compat : forall An x l, Rpser An x l -> Rpser (- An)%Rseq x (-l).
proof: Proof. intros An x l Hl eps eps_pos ; destruct (Hl _ eps_pos) as [N HN] ; exists N ; intros n n_lb ; unfold R_dist, Rminus in * ; rewrite Rseq_pps_opp_compat ; unfold Rseq_opp ; rewrite <- Ropp_plus_distr, Rabs_Ropp ; apply HN ; assumption. Qed.
imports: Reals Rpser_def Rpser_def_simpl Rinterval Rsequence_def Rsequence_base_facts Rsequence_subsequence Rsequence_rewrite_facts Rsequence_cv_facts Rsequence_facts Rsequence_bound_facts Rsequence_sums_facts Rpow_facts PeanoNat Lra MyRIneq MyNat MyNNR