fact: Definition diff_refining_points prec xi di yi yi' ym yl yu := match I.sign_large yi' with | Xund => if I.bounded yi' then I.meet yi (I.add prec ym (I.mul prec di yi')) else yi | Xeq => ym | Xlt => I.meet (if I.lower_bounded xi then I.lower_extent yl else I.whole) (if I.upper_bounded xi then I.upper_extent yu else I.whole) | Xgt => I.meet (if I.lower_bounded xi then I.upper_extent yl else I.whole) (if I.upper_bounded xi then I.lower_extent yu else I.whole) end.
imports: Coq(Bool Reals) Flocq(Zaux Raux) Coq(List) Coquelicot(Coquelicot) mathcomp.ssreflect(ssreflect) Stdlib Coquelicot Xreal Xreal_derive Basic Interval Interval_compl Taylor_model Tree Prog