proposition: Lemma Derive_partial_derive_aux2: forall p k f x y, locally_2d (ex_diff_n f (p+S k)) x y -> partial_derive 0 1 (partial_derive p k f) x y = partial_derive p (S k) f x y.
proof: Proof. intros p; induction p. intros; easy. intros k f x y Y. apply sym_eq. apply trans_eq with (partial_derive p 0 (partial_derive 1 (S k) f) x y). rewrite partial_derive_add_zero. rewrite Nat.add_0_l. replace (S p) with (p+1)%nat by apply Nat.add_comm. easy. now left. apply trans_eq with (partial_derive p 0 (partial_derive 0 (S k) (partial_derive 1 0 f)) x y). apply partial_derive_ext_loc. apply locally_2d_impl_strong with (2:=Y). apply locally_2d_forall. intros u v H. apply Derive_partial_derive_aux1. apply locally_2d_impl with (2:=H). apply locally_2d_forall. intros u'' v''. apply ex_diff_n_m. lia. apply trans_eq with (partial_derive p (S k) (partial_derive 1 0 f) x y). rewrite partial_derive_add_zero. now rewrite Nat.add_0_l Nat.add_0_r. now right. rewrite - IHp. apply partial_derive_ext_loc. apply locally_2d_impl_strong with (2:=Y). apply locally_2d_forall. intros u v H. apply trans_eq with (partial_derive p 0 (partial_derive 0 k (partial_derive 1 0 f)) u v). rewrite (partial_derive_add_zero _ _ 0%nat). now rewrite Nat.add_0_l Nat.add_0_r. now right. apply trans_eq with (partial_derive p 0 (partial_derive 1 k f) u v). apply partial_derive_ext_loc. apply locally_2d_impl_strong with (2:=H). apply locally_2d_forall. intros u' v' H'. apply sym_eq. apply Derive_partial_derive_aux1. apply locally_2d_impl with (2:=H'). apply locally_2d_forall. intros u'' v''. apply ex_diff_n_m. apply MyNat.le_add_l. rewrite partial_derive_add_zero. rewrite Nat.add_0_l. replace (S p) with (p+1)%nat by apply Nat.add_comm. easy. now left. apply locally_2d_impl with (2:=Y). apply locally_2d_forall. intros u'' v''. replace (p+ S k)%nat with ((S p+S k)-(1+0))%nat. apply ex_diff_n_deriv. now rewrite Nat.add_0_r Nat.add_succ_l; apply ->Nat.succ_le_mono; apply Nat.le_0_l. now rewrite Nat.add_0_r Nat.add_succ_l Nat.sub_succ Nat.sub_0_r. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Hierarchy Continuity Derive