fact: Definition lookup fi bounds idx extend steps := let bounds' := lookup_piece bounds idx steps in let output := extend (fi bounds') in if I.lower_bounded output || I.upper_bounded output then lookup_main fi bounds idx output steps else output.
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