proposition: Lemma Continuous_Int : forall (I : interval) (cI : compact_ I) H (F : PartIR), Continuous_I (a:=Lend cI) (b:=Rend cI) H F -> Continuous I F.
proof: Proof. intros I cI H F H0. cut (included I (compact (Lend cI) (Rend cI) H)). 2: apply interval_compact_inc; auto. cut (included (compact (Lend cI) (Rend cI) H) I). 2: apply compact_interval_inc; auto. generalize cI H H0; clear H0 H cI. destruct I as [| c| c| c| c| c c0| c c0| c c0| c c0]; intros; try inversion cI. generalize c c0 cI H H0 X X0; clear X0 X H0 H cI c0 c. simpl in |- *; intros a b Hab Hab' contF inc1 inc2. split. apply included_trans with (Compact Hab'); Included. intros. apply included_imp_contin with (Hab := Hab'); Included. Qed.
imports: CoRN.ftc.NthDerivative