fact: Definition derivable_oo_continuous_bnd (f : R -> V) (x y : R) := [/\ {in `]x, y[, forall x, derivable f x 1}, f @ x^'+ --> f x & f @ y^'- --> f y].
imports: mathcomp(all_ssreflect ssralg ssrint ssrnum finmap) mathcomp(matrix interval zmodp vector fieldext falgebra) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality) ereal reals signed topology prodnormedzmodule normedtype derive sequences real_interval HB(structures)