fact: Definition C_complete_lim (F : (C -> Prop) -> Prop) := (R_complete_lim (fun P => F (fun z => P (Re z))), R_complete_lim (fun P => F (fun z => P (Im z)))).
imports: Coq(Reals ssreflect) Rcomplements Rbar Continuity Derive Hierarchy