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