fact: Definition DL_regular_n f m x y := exists D, locally_2d (fun u v => Rabs (f u v - DL_pol m f x y (u-x) (v-y)) <= D * (Rmax (Rabs (u-x)) (Rabs (v-y))) ^ (S m)) x y.
imports: Coq(Reals Psatz ssreflect) Rcomplements Hierarchy Continuity Derive