proposition: Theorem eval_correct_ext : forall prec deg prog bounds vars, contains_all bounds vars -> forall n yi, I.extension (Xbind (fun x => nth n (eval_ext prog (Xreal x :: map Xreal vars)) Xnan)) (fun b => TM.eval (prec,deg) (nth n (eval prec deg yi prog (TM.var :: map TM.const bounds)) TM.dummy) yi b).
proof: Proof. intros prec deg prog bounds vars Hv n yi xi x Hx. apply (@TM.eval_correct (prec,deg) yi) with (2 := Hx). now apply eval_correct_aux. 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