proposition: Theorem eval_correct' : forall prec prog bounds vars, contains_all bounds vars -> forall n, contains (I.convert (nth n (eval prec prog bounds) I.nai)) (Xreal (nth n (eval_real prog vars) 0%R)).
proof: Proof. intros prec prog bounds vars H n. set (yi := nth n _ _). apply (xreal_to_real (fun y => contains (I.convert yi) y) (fun y => contains (I.convert yi) (Xreal y))). now destruct (I.convert yi). easy. now apply eval_correct. Qed.
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