proposition: Lemma diffble_imp_contin_I : forall a b (Hab' : a [<] b) (Hab : a [<=] b) F, Diffble_I Hab' F -> Continuous_I Hab F.
proof: Proof. intros a b Hab' Hab F H. apply deriv_imp_contin_I with Hab' (PartInt (ProjT1 H)). apply projT2. Qed.
imports: CoRN.ftc.PartInterval CoRN.ftc.DerivativeOps