fact: Definition fast_enough prec xi xi' := if I.bounded xi then let (xi1, _) := I.bisect xi in I.wider prec xi1 xi' else I.bounded xi'.
imports: Coq(Reals List ZArith Psatz) Flocq(Zaux) Stdlib Xreal Basic Sig Interval Eval Tree Prog Reify Interval_helper