Lemma absCC_absIR_re : forall x : C, AbsIR (ℜ x) [<=] AbsCC x.


Lemma absCC_absIR_im : forall x : C, AbsIR (ℑ x) [<=] AbsCC x.


Definition seq_re (s : N -> C) (n : N) := ℜ (s n).
Definition seq_im (s : N -> C) (n : N) := ℑ (s n).

Definition CC_Cauchy_prop (s : N -> C) : CProp :=
  Cauchy_prop (seq_re s) and Cauchy_prop (seq_im s).

Record CC_CauchySeq : Type :=
 {CC_seq :> N -> C;
  CC_proof : CC_Cauchy_prop CC_seq}.

Lemma re_is_Cauchy : forall s : CC_CauchySeq, Cauchy_prop (seq_re s).

Lemma im_is_Cauchy : forall s : CC_CauchySeq, Cauchy_prop (seq_im s).

Definition CC_Cauchy2re s := Build_CauchySeq _ _ (re_is_Cauchy s).

Definition CC_Cauchy2im s := Build_CauchySeq _ _ (im_is_Cauchy s).

Definition LimCC s : C := (Lim (CC_Cauchy2re s)) [+I*] (Lim (CC_Cauchy2im s)).

Definition CC_SeqLimit (seq : N -> C) (lim : C) : CProp := forall e,
  0 [<] e -> {N : N | forall m, N <= m -> AbsCC (seq m[-]lim) [<=] e}.

Lemma AbsSmall_sqr : forall x e : IR, AbsSmall e x -> x[^]2 [<=] e[^]2.




Lemma AbsSmall_AbsCC : forall (z : C) (e : IR), 0 [<] e ->
 AbsSmall (e [/]2) (ℜ z) -> AbsSmall (e [/]2) (ℑ z) -> AbsCC z [<=] e.








Lemma LimCC_is_lim : forall s : CC_CauchySeq, CC_SeqLimit s (LimCC s).














Lemma CC_SeqLimit_uniq : forall (s : N -> C) (l l' : C),
 CC_SeqLimit s l -> CC_SeqLimit s l' -> l [=] l'.














Lemma CC_SeqLimit_unq : forall (s : CC_CauchySeq) l, CC_SeqLimit s l -> l [=] LimCC s.

Section Continuity_for_CC.

Variable f : C -> C.

Definition CCfunLim (p l : C) : CProp := forall e : IR, 0 [<] e ->
  {d : IR | 0 [<] d | forall x, AbsCC (p[-]x) [<=] d -> AbsCC (l[-]f x) [<=] e}.

Definition CCcontinAt p : CProp := CCfunLim p (f p).

Definition CCcontin : CProp := forall x : C, CCcontinAt x.

Lemma CCfunLim_SeqLimit : forall p l pn,
 CCfunLim p l -> CC_SeqLimit pn p -> CC_SeqLimit (fun n => f (pn n)) l.


Definition f_seq (s : N -> C) (n : N) : C := f (s n).

Lemma poly_pres_lim : CCcontin ->
 forall s : CC_CauchySeq, CC_SeqLimit (fun n => f (s n)) (f (LimCC s)).

End Continuity_for_CC.

Lemma seq_yields_zero : forall q : IR, 0 [<=] q -> q [<] 1 -> forall c : IR, 0 [<] c ->
 forall s, (forall i, AbsCC (s i) [<=] q[^]i[*]c) -> CC_SeqLimit s 0.