proposition: Theorem eval_bisect_correct : forall prec depth idx vars hyps prog consts g, eval_bisect prec depth idx hyps prog consts g = true -> eval_hyps hyps vars (eval_goal g (eval_real' prog vars consts)).
proof: Proof. intros prec depth idx vars hyps prog consts g H. apply eval_bisect_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