proposition: Lemma Derive_partial_derive_aux1: forall p f x y, locally_2d (ex_diff_n f (S p)) x y -> partial_derive 1 p f x y = partial_derive 0 p (partial_derive 1 0 f) x y.
proof: Proof. intros p; induction p. intros f x y H. unfold partial_derive; now simpl. intros f x y H. apply trans_eq with (partial_derive 1 p (partial_derive 0 1 f) x y). unfold partial_derive. simpl. apply Derive_ext. intros t. apply trans_eq with (Derive_n (Derive_n (fun z : R => f t z) p) 1 y). reflexivity. rewrite Derive_n_comp. rewrite Nat.add_comm. rewrite -Derive_n_comp. reflexivity. rewrite IHp. apply trans_eq with (partial_derive 0 p (partial_derive 0 1 (partial_derive 1 0 f)) x y). unfold partial_derive. simpl. apply Derive_n_ext_loc. cut (locally_2d (fun u v => Derive (fun x0 : R => Derive (fun x1 : R => f x0 x1) v) u = Derive (fun x0 : R => Derive (fun x1 : R => f x1 x0) u) v) x y). apply locally_2d_1d_const_x. apply locally_2d_impl_strong with (2:=H). apply locally_2d_forall. intros u v H1. apply Schwarz. apply locally_2d_impl with (2:=H1). apply locally_2d_forall. intros u' v' H2. split. apply H2. split. apply H2. simpl in H2; destruct H2 as (T1&T2&T3&T4&T5). split. apply T5. apply T4. apply locally_2d_singleton in H1. simpl in H1; destruct H1 as (T1&T2&T3&T4&T5). destruct T5 as (Y1&Y2&Y3&Y4&Y5). clear - Y4. case p in Y4; simpl in Y4; apply Y4. apply locally_2d_singleton in H1. simpl in H1; destruct H1 as (T1&T2&T3&T4&T5). destruct T4 as (Y1&Y2&Y3&Y4&Y5). clear - Y5. case p in Y5; simpl in Y5; apply Y5. unfold partial_derive. simpl. apply trans_eq with (Derive_n (Derive_n (fun z => Derive (fun x0 => f x0 z) x) p) 1 y). rewrite Derive_n_comp. rewrite Nat.add_comm. rewrite -Derive_n_comp. reflexivity. reflexivity. apply locally_2d_impl with (2:=H). apply locally_2d_forall. intros u v. pattern (S p) at 2; replace (S p) with (S (S p) -(0+1))%nat. apply ex_diff_n_deriv. rewrite Nat.add_0_l; apply ->Nat.succ_le_mono; exact (Nat.le_0_l _). by rewrite Nat.add_0_l Nat.sub_succ Nat.sub_0_r. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Hierarchy Continuity Derive