fact: Definition derivable_pt_lim f (x l:R) : Prop := forall eps:R, 0 < eps -> exists delta : posreal, (forall h:R, h <> 0 -> Rabs h < delta -> Rabs ((f (x + h) - f x) / h - l) < eps).
imports: Rbase Rfunctions Rlimit Rderiv