proposition: Lemma Cseq_cv_add_compat : Cseq_cv (Un + Vn) (lu + lv).
proof: Proof. intros 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 Cseq_add. replace (Un n + Vn n - (lu + lv))%C with ((Un n - lu) + (Vn n - lv))%C by field. eapply Rle_lt_trans; [apply Cnorm_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: MyReals PeanoNat Rsequence_def Rsequence_facts Rsequence_base_facts Lia Lra Complex Csequence_def