proposition: Lemma Cseq_cv_eq_compat : forall l, (forall n, Un n = Vn n) -> Cseq_cv Un l -> Cseq_cv Vn l.
proof: Proof. intros l H Hl eps Heps. destruct (Hl eps Heps) as [N HN]; exists N; intros n Hn; rewrite <- H; apply HN; apply Hn. Qed.
imports: MyReals PeanoNat Rsequence_def Rsequence_facts Rsequence_base_facts Lia Lra Complex Csequence_def