fact: Fixpoint bisect bounds idx check steps { struct steps } := match steps, idx with | O, _ => check bounds | S _, nil => check bounds | S steps, i :: idx => let idx := app idx (i :: nil) in bisect_step bounds i check (fun b => bisect b idx check 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