proposal renaming for `derivable_oo_continuous_bnd`

[affeldt-aist]

analysis/theories/realfun.v

Line 24 in 6600f40

(* derivable_oo_continuous_bnd f x y == f is derivable in `]x, y[ and *)

here we use the suffix _bnd to mean "the left/right boundaries" but we have also been using bnd when lemmas are about intervals the boundaries of which we do not need to commit (and therefore use more generally itv_bound instead of open/close) which is not really the case here.

What about removing the prefix _bnd or (better) replacing continuous_bnd with, say, leftright_continuous, right_continuous, etc. like the notation we introduced in lebesgue_stieltjes_measure.v? It would look more consistent.

@zstone1 @CohenCyril @IshiguroYoshihiro