fact: Fixpoint lookup_piece bounds idx steps { struct steps } := match steps, idx with | O, _ => bounds | S _, nil => bounds | S steps, i :: idx => let idx := app idx (i :: nil) in let bounds := change_nth i bounds (fun xi => fst (I.bisect xi)) in lookup_piece bounds idx 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