proposition: Lemma Int_Continuous : forall (I : interval) (cI : compact_ I) H (F : PartIR), Continuous I F -> Continuous_I (a:=Lend cI) (b:=Rend cI) H F.
proof: Proof. intros [| c| c| c| c| c c0| c c0| c c0| c c0]; intros; try inversion cI. generalize c c0 cI H F X; clear X F H cI c0 c. simpl in |- *; intros a b Hab Hab' F contF. inversion_clear contF. Contin. Qed.
imports: CoRN.ftc.NthDerivative