proposition: Lemma Cseq_cst_cv : forall (c : C), Cseq_cv (fun _ => c) c.
proof: Proof. intros c eps Heps; exists O; intros n Hn. unfold R_dist. assert (c - c = C0)%C. ring. rewrite H. change (Cnorm C0 < eps). rewrite Cnorm_C0; apply Heps. Qed.
imports: MyReals PeanoNat Rsequence_def Rsequence_facts Rsequence_base_facts Lia Lra Complex Csequence_def