proposition: Lemma ex_diff_n_deriv_aux2: forall f n x y, ex_diff_n f (S n) x y -> ex_diff_n (fun u v => Derive (fun z => f u z) v) n x y.
proof: Proof. intros f n x y. case n. simpl. intros H; split; apply H. clear n;intros n H. simpl in H. repeat split; apply H. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Hierarchy Continuity Derive