proposition: Lemma contin_polyCC : CCcontin (fun x => g ! x).
proof: Proof. unfold CCcontin in |- *. unfold CCcontinAt in |- *. unfold CCfunLim in |- *. intros. elim (cpoly_CC_contin x e); auto. intro d. intros H0 H1. exists d. auto. intros. apply H1; auto. Qed.
imports: CoRN.fta.CC_Props