proposition: Theorem eval_bisect_contains_diff_correct : forall prec depth idx vars hyps prog consts b, eval_bisect_contains_diff 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. destruct xi as [|xi li]. apply J.nai_correct. destruct Ix as [H1 H2]. destruct x as [|x l]. easy. apply A.DiffValuator.eval_correct. split. now injection H1. intros n. apply (H2 (S n)). apply (H2 O). Qed.
imports: Coq(Reals List ZArith Psatz) Flocq(Zaux) Stdlib Xreal Basic Sig Interval Eval Tree Prog Reify