fact: Definition diff_refining prec xi yi yi' fi := match I.sign_large yi' with | Xund => if I.bounded yi' then let mi := J.midpoint xi in I.meet yi (I.add prec (fi mi) (I.mul prec (I.sub prec xi mi) yi')) else yi | Xeq => fi (J.midpoint xi) | Xlt => I.meet (if I.lower_bounded xi then let l := I.lower xi in I.lower_extent (fi (I.bnd l l)) else I.whole) (if I.upper_bounded xi then let u := I.upper xi in I.upper_extent (fi (I.bnd u u)) else I.whole) | Xgt => I.meet (if I.lower_bounded xi then let l := I.lower xi in I.upper_extent (fi (I.bnd l l)) else I.whole) (if I.upper_bounded xi then let u := I.upper xi in I.lower_extent (fi (I.bnd u u)) 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