proposition: Lemma CCfunLim_SeqLimit : forall p l pn, CCfunLim p l -> CC_SeqLimit pn p -> CC_SeqLimit (fun n => f (pn n)) l.
proof: Proof. intros p l pn fl sl; unfold CC_SeqLimit in |- *. intros eps epos. elim (fl _ epos); intros del H H0. elim (sl _ H); intros N Nh. exists N. intros m leNm. apply leEq_wdl with (AbsCC (l[-]f (pn m))). apply H0. apply leEq_wdl with (AbsCC (pn m[-]p)). apply (Nh _ leNm). apply cc_minus_abs. apply cc_minus_abs. Qed.
imports: CoRN.complex.AbsCC Coq(Lia)