fact: Definition DL_pol (n : nat) (f : R -> R -> R) (x y dx dy : R) : R := sum_f_R0 (fun p => differential p f x y dx dy / INR (fact p)) n.
imports: Coq(Reals Psatz ssreflect) Rcomplements Hierarchy Continuity Derive