fact: Fixpoint lookup_main fi bounds idx output steps { struct steps } := match steps, idx with | O, _ => I.join (fi bounds) output | S _, nil => I.join (fi bounds) output | S steps, i :: idx => let idx := app idx (i :: nil) in lookup_step fi bounds i output (fun bounds output => lookup_main fi bounds idx output steps) 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