fact: Definition bisect_step (bounds : list I.type) i (check : list I.type -> bool) cont := if check bounds then true else let bounds' := change_nth i bounds (fun xi => fst (I.bisect xi)) in match cont bounds' with | true => let bounds' := change_nth i bounds (fun xi => snd (I.bisect xi)) in cont bounds' | false => false 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