proposition: Lemma Derivative_n_imp_Continuous : forall n F G, 0 < n -> Derivative_n n I pI F G -> Continuous I F.
proof: Proof. intros n F G H H0. cut (Diffble I pI F). intro H1. apply Derivative_imp_Continuous with pI (Deriv _ H1). apply Deriv_lemma. apply Diffble_n_imp_Diffble with n; auto. apply Derivative_n_imp_Diffble_n with G; auto. Qed.
imports: CoRN.ftc.MoreIntervals