proposition: Lemma ex_diff_n_continuity_inf_2 : 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 u z) v) x y.
proof: Proof. intros n p k Hn f x y Hf. assert (ex_diff_n (partial_derive p k f) (n -(p+k)) x y). apply ex_diff_n_deriv. now apply Nat.lt_le_incl. exact Hf. revert H; case_eq (n-(p+k))%nat. intros H; contradict Hn. lia. intros n0 Hn0; simpl; intros (T1&T2&T3&T4&T5). revert T5; case n0. intros Y; apply Y. intros n1 Y; apply Y. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Hierarchy Continuity Derive