proposition: Lemma Cseq_cv_re_im_compat : forall Un l, Rseq_cv (fun n => Cre (Un n)) (Cre l) -> Rseq_cv (fun n => Cim (Un n)) (Cim l) -> Cseq_cv Un l.
proof: Proof. intros Un l Hre Him e epos. pose (e / 2)%R as e'. assert (e'pos : e' > 0) by (unfold e'; lra). destruct (Hre e' e'pos) as [Nre HNre]. destruct (Him e' e'pos) as [Nim HNim]. exists (Nat.max Nre Nim). intros n Hn. replace e with (e' + e')%R by (unfold e'; field). eapply Rle_lt_trans. apply Cnorm_le_Cre_Cim. apply Rplus_lt_compat. rewrite <- Cre_minus_compat. apply HNre. eapply Nat.le_trans. apply Nat.le_max_l. apply Hn. rewrite <- Cim_minus_compat. apply HNim. eapply Nat.le_trans. apply Nat.le_max_r. apply Hn. Qed.
imports: MyReals PeanoNat Rsequence_def Rsequence_facts Rsequence_base_facts Lia Lra Complex Csequence_def