proposition: Lemma Derivative_n_imp_Diffble : forall n, 0 < n -> forall F F', Derivative_n n I pI F F' -> Diffble I pI F.
proof: Proof. intros n H F F' H0. elim H0; intros incF H1. elim H1; intros incF' derivF. split; auto. intros; apply deriv_n_imp_diffble with n F'; auto. Qed.
imports: CoRN.ftc.MoreIntervals