proposition: Theorem eval_correct_ext' : forall prec prog bounds vars, contains_all bounds vars -> forall xi x, contains (I.convert xi) (Xreal x) -> forall n, contains (I.convert (nth n (eval prec prog (xi :: bounds)) I.nai)) (Xreal (nth n (eval_real prog (x :: vars)) 0%R)).
proof: Proof. intros prec prog bounds vars [H1 H2] xi x Hx. apply eval_correct'. now apply contains_all_cons. 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