proposition: Theorem eval_correct_ext : forall prec prog bounds vars, contains_all bounds vars -> forall n, I.extension (fun x => nth n (eval_ext prog (x :: map Xreal vars)) Xnan) (fun b => nth n (eval prec prog (b :: bounds)) I.nai).
proof: Proof. intros prec prog bounds vars H n xi x Hx. revert n. apply eval_correct_aux. intros [|n]. exact Hx. simpl. 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