proposition: Lemma Deriv_lemma : forall F diffF, Derivative I pI F (Deriv F diffF).
proof: Proof. intros; unfold Deriv in |- *. apply Derivative_wdl with (N_Deriv 0 F (le_imp_Diffble_n 0 1 (Nat.le_succ_diag_r 0) F (Diffble_imp_Diffble_n _ diffF))). apply Derivative_n_unique with 0 F. apply N_Deriv_lemma. apply Derivative_n_O; elim diffF; auto. apply N_Deriv_S. Qed.
imports: CoRN.ftc.MoreIntervals