proposition: Lemma Rseq_cv_plus_compat : forall Un Vn lu lv, Rseq_cv Un lu -> Rseq_cv Vn lv -> Rseq_cv (Un + Vn) (lu + lv).
proof: Proof. intros Un Vn lu lv Hu Hv eps Heps. destruct (Hu (eps/2)%R) as [Nu HNu]; [lra|]. destruct (Hv (eps/2)%R) as [Nv HNv]; [lra|]. exists (Nat.max Nu Nv). intros n Hn. unfold R_dist; unfold Rseq_plus. replace (Un n + Vn n - (lu + lv))%R with ((Un n - lu) + (Vn n - lv))%R by field. eapply Rle_lt_trans; [apply Rabs_triang|]. replace eps with (eps/2 + eps/2)%R by field. apply Rplus_lt_compat. apply (HNu n); eapply Nat.le_trans; [apply Nat.le_max_l|eexact Hn]. apply (HNv n); eapply Nat.le_trans; [apply Nat.le_max_r|eexact Hn]. Qed.
imports: Lia Rsequence_def Rsequence_base_facts PeanoNat Rinterval MyRIneq Ranalysis_def Lra