proposition: Lemma poly_pres_lim : CCcontin -> forall s : CC_CauchySeq, CC_SeqLimit (fun n => f (s n)) (f (LimCC s)).
proof: Proof. intros cp s. apply (CCfunLim_SeqLimit (LimCC s) (f (LimCC s))). unfold CCfunLim in |- *. intros e zlte. elim (cp (LimCC s) e zlte). intros d; exists d; auto. exact (LimCC_is_lim s). Qed.
imports: CoRN.complex.AbsCC Coq(Lia)