proposition: Lemma Cseq_cv_re_compat : forall Un l, Cseq_cv Un l -> Rseq_cv (fun n : nat => Cre (Un n)) (Cre l).
proof: Proof. intros Un l HC e epos. destruct (HC e epos) as [N HN]; exists N. intros n Hn. pose proof HN n Hn. unfold R_dist. rewrite Cre_minus_compat. eapply Rle_lt_trans. apply Cre_le_Cnorm. auto. Qed.
imports: MyReals PeanoNat Rsequence_def Rsequence_facts Rsequence_base_facts Lia Lra Complex Csequence_def