proposition: Lemma Derivative_imp_Diffble : forall F F', Derivative I pI F F' -> Diffble I pI F.
proof: Proof. intros F F' H. elim H; intros incF H'. elim H'; intros incF' derivF. split; auto. intros; apply deriv_imp_Diffble_I with F'; auto. Qed.
imports: CoRN.ftc.MoreIntervals