proposition: Lemma ex_diff_n_deriv: forall n p q, (p+q <= n)%nat -> forall f x y, ex_diff_n f n x y-> ex_diff_n (partial_derive p q f) (n -(p+q)) x y.
proof: Proof. induction p. intros q; rewrite Nat.add_0_l. induction q. intros H f x y H1. unfold partial_derive. simpl. rewrite Nat.sub_0_r. apply: (ex_diff_n_ext_loc _ _ _ _ _ _ H1). now apply locally_2d_forall. intros H f x y H1. apply (ex_diff_n_ext_loc (fun u v => Derive (fun z => (partial_derive 0 q f) u z) v)). apply locally_2d_forall. intros u v; unfold partial_derive. reflexivity. apply ex_diff_n_deriv_aux2. replace ((S (n - S q))) with (n-q)%nat by lia. apply IHq. now apply Nat.lt_le_incl. exact H1. intros q H f x y H1. apply (ex_diff_n_ext_loc (fun u v => Derive (fun z => (partial_derive p q f) z v) u)). apply locally_2d_forall. intros u v; unfold partial_derive. reflexivity. apply ex_diff_n_deriv_aux1. replace ((S (n - (S p +q)))) with (n-(p+q))%nat by lia. apply IHp. now apply Nat.lt_le_incl. exact H1. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Hierarchy Continuity Derive