proposition: Lemma Cseq_cv_opp_compat : Cseq_cv (- Un) (- lu).
proof: Proof. intros eps Heps. destruct (Hu eps) as [Nu HNu]; [assumption|]. exists Nu; intros n Hn. unfold R_dist; unfold Cseq_opp. replace (- Un n - - lu)%C with (- (Un n - lu))%C by field. rewrite Cnorm_opp. apply HNu; exact Hn. Qed.
imports: MyReals PeanoNat Rsequence_def Rsequence_facts Rsequence_base_facts Lia Lra Complex Csequence_def