proposition: Lemma Cseq_cv_cnorm_compat : Rseq_cv (fun k => Cnorm (Un k)) (Cnorm lu).
proof: Proof. intros eps Heps ; destruct (Hu eps Heps) as [N HN]. exists N. intros n Hn. unfold R_dist. apply Rle_lt_trans with (Cnorm (Un n - lu)). apply Cnorm_triang_rev. apply HN; apply Hn. Qed.
imports: MyReals PeanoNat Rsequence_def Rsequence_facts Rsequence_base_facts Lia Lra Complex Csequence_def