proposition: Lemma LimCC_is_lim : forall s : CC_CauchySeq, CC_SeqLimit s (LimCC s).
proof: Proof. unfold CC_SeqLimit in |- *. unfold LimCC in |- *. intros s e H. cut (SeqLimit (seq_re s) (Lim (CC_Cauchy2re s))). unfold SeqLimit in |- *. intro H0. cut (SeqLimit (seq_im s) (Lim (CC_Cauchy2im s))). unfold SeqLimit in |- *. intro H1. cut ([0] [<] e [/]TwoNZ). intro H2. elim (H0 (e [/]TwoNZ) H2). unfold seq_re in |- *. intro N. intros H3. elim (H1 (e [/]TwoNZ) H2). unfold seq_im in |- *. intro N'. intros H4. cut {M : nat | N <= M | N' <= M}. intros H5. elim H5. clear H5. intro M. intros. exists M. intros. apply AbsSmall_AbsCC. auto. astepr (Re (CC_seq s m) [-]Lim (CC_Cauchy2re s)). apply H3. lia. astepr (Im (CC_seq s m) [-]Lim (CC_Cauchy2im s)). apply H4. lia. elim (le_lt_dec N N'); intros. exists N'; auto. exists N; auto with arith. apply div_resp_pos. apply pos_two. auto. apply Lim_Cauchy with (s := Build_CauchySeq IR (fun n : nat => Im (CC_seq s n)) (im_is_Cauchy s)). apply Lim_Cauchy with (s := Build_CauchySeq IR (fun n : nat => Re (CC_seq s n)) (re_is_Cauchy s)). Qed.
imports: CoRN.complex.AbsCC Coq(Lia)