proposition: Theorem eval_bisect_contains_correct : forall prec depth idx vars hyps prog consts b, eval_bisect_contains prec depth idx hyps prog consts b = true -> eval_hyps hyps vars (contains (I.convert b) (Xreal (eval_real' prog vars consts))).
proof: Proof. intros prec depth idx vars hyps prog consts b H. apply eval_bisect_contains_aux with (2 := H). intros xi x Ix. now apply A.BndValuator.eval_correct'. Qed.
imports: Coq(Reals List ZArith Psatz) Flocq(Zaux) Stdlib Xreal Basic Sig Interval Eval Tree Prog Reify