proposition: Lemma Derive_partial_derive: forall p k f x y, locally_2d (ex_diff_n f (p+S k)) x y -> Derive (fun v : R => partial_derive p k f x v) y = partial_derive p (S k) f x y.
proof: Proof. intros p k f x y H. generalize (Derive_partial_derive_aux2 p k f x y H). easy. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Hierarchy Continuity Derive