proposition: Lemma partial_derive_ext_loc : forall f g p q x y, locally_2d (fun u v => f u v = g u v) x y -> partial_derive p q f x y = partial_derive p q g x y.
proof: Proof. intros f g p q x y H. unfold partial_derive. apply Derive_n_ext_loc. destruct H as (e,He). exists e. intros u Hu. apply Derive_n_ext_loc. exists e. intros v Hv. now apply He. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Hierarchy Continuity Derive