fact: Definition C_lim (f : C -> C) (z : C) : C := (real (Lim (fun x => fst (f (x, snd z))) (fst z)), real (Lim (fun x => snd (f (x, snd z))) (fst z))).
imports: Coq(Reals ssreflect) Rcomplements Rbar Continuity Derive Hierarchy