proposition: Lemma Derivative_imp_Continuous : Derivative I pI F G -> Continuous I F.
proof: Proof. intro H0. elim H0; intros incF H'. elim H'; intros incG derF. clear H0 H'. split. Included. intros a b Hab H0. elim (compact_proper_in_interval _ _ _ Hab H0 pI); intros a' Ha. elim Ha; clear Ha; intros b' Hb. elim Hb; clear Hb; intros Hab' H2 H3. apply included_imp_contin with (Hab := less_leEq _ _ _ Hab'). auto. apply deriv_imp_contin_I with Hab' G; auto. Qed.
imports: CoRN.ftc.MoreIntervals