fact: Definition eval_bisect_diff_fun prec prog xi := match xi with | nil => I.nai | xi :: li => A.DiffValuator.eval prec prog li 0 xi end.
imports: Coq(Reals List ZArith Psatz) Flocq(Zaux) Stdlib Xreal Basic Sig Interval Eval Tree Prog Reify