proposition: Lemma partial_derive_add_zero: forall f p q r s x y, (q=0)%nat \/ (r=0)%nat -> partial_derive p q (partial_derive r s f) x y = partial_derive (p+r) (q+s) f x y.
proof: Proof. intros f p q r s x y H. destruct H; rewrite H. rewrite Nat.add_0_l. unfold partial_derive. simpl. rewrite -Derive_n_comp. now apply Derive_n_ext. rewrite Nat.add_0_r. unfold partial_derive. simpl. apply Derive_n_ext. intros y0. rewrite -Derive_n_comp. now apply Derive_n_ext. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Hierarchy Continuity Derive