fact: Definition partial_derive (m k : nat) (f : R -> R -> R) : R -> R -> R := fun x y => Derive_n (fun t => Derive_n (fun z => f t z) k y) m x.
imports: Coq(Reals Psatz ssreflect) Rcomplements Hierarchy Continuity Derive