fact: Definition root prec formula bounds xi := match nth 0 (eval_generic (diff_operations _ (BndValuator.operations prec)) formula ((xi, I.mask (I.fromZ_small 1) xi) :: map (fun b => (b, I.mask I.zero xi)) bounds)) (I.nai, I.nai) with | (yi, yi') => match I.sign_strict yi with | Xlt | Xgt => I.empty | _ => let mi := J.midpoint xi in let yi := nth 0 (BndValuator.eval prec formula (mi :: bounds)) I.nai in I.meet xi (I.sub prec mi (I.div prec yi yi')) end 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