proposition: Lemma Exp_unique_lemma : forall H F, Derivative realline H F F -> forall n, Derivative_n n realline H F F.
proof: Proof. intros H F H0 n; induction n as [| n Hrecn]. apply Derivative_n_O; Included. apply Derivative_n_plus with n 1 F; auto. apply Derivative_n_1; auto. Qed.
imports: CoRN.transc.TaylorSeries