proposition: Lemma Cseq_cv_unique : forall Un lu1 lu2, Cseq_cv Un lu1 -> Cseq_cv Un lu2 -> lu1 = lu2.
proof: Proof. intros Un l1 l2 Hl1 Hl2. rewrite <- Cproj_right with l1. rewrite <- Cproj_right with l2. cut (Cre l1 = Cre l2 /\ Cim l1 = Cim l2). intros [H I]; rewrite H; rewrite I; trivial. split. apply Rseq_cv_unique with (fun n => Cre (Un n)); apply Cseq_cv_re_compat; assumption. apply Rseq_cv_unique with (fun n => Cim (Un n)); apply Cseq_cv_im_compat; assumption. Qed.
imports: MyReals PeanoNat Rsequence_def Rsequence_facts Rsequence_base_facts Lia Lra Complex Csequence_def