proposition: Lemma Cseq_cv_minus_compat : Cseq_cv (Un - Vn) (lu - lv).
proof: Proof. apply Cseq_cv_eq_compat with (Un + (-Vn)). reflexivity. apply Cseq_cv_add_compat. apply Hu. apply Cseq_cv_opp_compat. apply Hv. Qed.
imports: MyReals PeanoNat Rsequence_def Rsequence_facts Rsequence_base_facts Lia Lra Complex Csequence_def