proposition: Lemma ex_diff_n_ex_deriv_inf_1 : forall n p k, (p+k < n)%nat -> forall f x y, ex_diff_n f n x y -> ex_derive (fun z : R => partial_derive p k f z y) x.
proof: Proof. intros n p; case p; clear p. intros k; case k; clear k. case n; clear n. intros Hn; contradict Hn; apply Nat.nlt_0_r. intros n _ f x y H. unfold partial_derive; simpl. apply H. intros n0 H f x y Hf. assert (ex_diff_n (partial_derive 0 n0 f) (n -(0+n0)) x y). apply ex_diff_n_deriv. auto with zarith. exact Hf. revert H0; rewrite Nat.add_0_l. case_eq (n-n0)%nat. intros H1; contradict H; auto with zarith. intros n1 H1 H2. apply ex_derive_ext with (fun z => Derive (fun t => (partial_derive 0 n0 f z) t) y). intros y0; unfold partial_derive; simpl. reflexivity. simpl in H2. destruct H2 as (T1&T2&T3&T4&T5). case_eq n1. intros H2; rewrite H2 in H1. clear -H H1; contradict H; auto with zarith. intros n2 Hn2; rewrite Hn2 in T5. apply T5. intros p q H f x y Hf. assert (ex_diff_n (partial_derive p q f) (n -(p+q)) x y). apply ex_diff_n_deriv. auto with zarith. exact Hf. case_eq (n-(p+q))%nat. intros H1; contradict H; auto with zarith. intros n1 H1. apply ex_derive_ext with (fun z => Derive (fun t => (partial_derive p q f t) y) z). intros x0; unfold partial_derive; simpl. reflexivity. rewrite H1 in H0; simpl in H0. destruct H0 as (T1&T2&T3&T4&T5). case_eq n1. intros H2; rewrite H2 in H1. clear -H H1; contradict H; auto with zarith. intros n2 Hn2; rewrite Hn2 in T4. apply T4. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Hierarchy Continuity Derive