proposition: Lemma ex_diff_n_continuity_inf_1 : forall n p k, (p+k < n)%nat -> forall f x y, ex_diff_n f n x y -> continuity_2d_pt (fun u v => Derive (fun z : R => partial_derive p k f z v) u) x y.
proof: Proof. intros n p k Hn f x y Hf. assert (ex_diff_n (partial_derive (S p) k f) (n -(S p+k)) x y). now apply ex_diff_n_deriv. apply continuity_2d_pt_ext_loc with (partial_derive (S p) k f). apply locally_2d_forall. intros u v; unfold partial_derive; simpl. reflexivity. revert H; case (n - (S p + k))%nat. simpl; intros H; apply H. intros n0; simpl; intros H; apply H. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Hierarchy Continuity Derive