proposition: Theorem eval_correct : forall prec prog bounds vars, contains_all bounds vars -> forall n xi x, contains (I.convert xi) (Xreal x) -> contains (I.convert (eval prec prog bounds n xi)) (Xreal (nth n (eval_real prog (x :: vars)) 0%R)).
proof: Proof. intros prec prog bounds vars Hv n xi x Hx. set (yi := eval prec prog _ n xi). 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. simpl. apply eval_correct_ext with (1 := Hv) (2 := Hx). 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