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)) (nth n (eval_ext prog (map Xreal vars)) Xnan).
proof: Proof. intros prec prog bounds vars H. apply eval_correct_aux. now apply contains_map_Xreal. 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