fact: Definition derivable_pt_lim f (x l : C) : Prop := forall eps:R, 0 < eps -> exists delta : posreal, forall h : C, h <> 0 -> Cnorm h < delta -> Cnorm ((f (x + h) - f x) / h - l) < eps.
imports: Cbase Cprop_base Cfunctions Cmet Cderiv