fact: Definition differential (p : nat) (f : R -> R -> R) (x y dx dy : R) : R := sum_f_R0 (fun m => C p m * partial_derive m (p - m)%nat f x y * dx ^ m * dy ^ (p - m)%nat) p.
imports: Coq(Reals Psatz ssreflect) Rcomplements Hierarchy Continuity Derive