proposition: Lemma derivable_oo_continuous_bnd_within (f : R -> V) (x y : R) : derivable_oo_continuous_bnd f x y -> {within `[x, y], continuous f}.
proof: Proof. move=> [fxy fxr fyl]; apply/subspace_continuousP => z /=. rewrite in_itv/= => /andP[]; rewrite le_eqVlt => /predU1P[<-{z} xy|]. have := cvg_at_right_within fxr; apply: cvg_trans; apply: cvg_app. by apply: within_subset => z/=; rewrite in_itv/= => /andP[]. move=> /[swap]. rewrite le_eqVlt => /predU1P[->{z} xy|zy xz]. have := cvg_at_left_within fyl; apply: cvg_trans; apply: cvg_app. by apply: within_subset => z/=; rewrite in_itv/= => /andP[]. apply: cvg_within_filter. apply/differentiable_continuous; rewrite -derivable1_diffP. by apply: fxy; rewrite in_itv/= xz zy. Qed.
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)