proposition: Lemma Derivative_n_imp_Continuous' : forall n F G, 0 < n -> Derivative_n n I pI F G -> Continuous I G.
proof: Proof. intros n F G H H0. cut (Diffble_n (pred n) I pI F). intro H1. apply Derivative_imp_Continuous' with pI (N_Deriv _ _ H1). apply Derivative_wdr with (N_Deriv _ _ (Derivative_n_imp_Diffble_n _ _ _ H0)). apply Derivative_n_unique with n F; auto; apply N_Deriv_lemma. cut (n = S (pred n)); [ intro | symmetry; apply Nat.lt_succ_pred with 0; auto ]. generalize H0 H1. rewrite H2. intros. apply N_Deriv_S. apply le_imp_Diffble_n with n. auto with arith. apply Derivative_n_imp_Diffble_n with G; auto. Qed.
imports: CoRN.ftc.MoreIntervals