proposition: Lemma Rpser_add_compat : forall An Bn x la lb, Rpser An x la -> Rpser Bn x lb -> Rpser (An + Bn)%Rseq x (la + lb).
proof: Proof. intros An Bn x la lb Hla Hlb eps eps_pos. pose (eps' := middle 0 eps) ; assert (eps'_pos : 0 < eps') by (apply middle_is_in_the_middle ; assumption). destruct (Hla _ eps'_pos) as [Na HNa] ; destruct (Hlb _ eps'_pos) as [Nb HNb] ; exists (Nat.max Na Nb) ; intros n n_lb. rewrite Rseq_pps_plus_compat ; eapply Rle_lt_trans. eapply R_dist_plus. apply Rlt_le_trans with (eps' + eps'). eapply Rlt_trans. eapply Rplus_lt_compat_l ; eapply HNb ; apply Nat.le_trans with (Nat.max Na Nb) ; [apply Nat.le_max_r | assumption]. apply Rplus_lt_compat_r ; apply HNa ; apply Nat.le_trans with (Nat.max Na Nb) ; [apply Nat.le_max_l | assumption]. right ; unfold eps', middle ; field. 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