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