proposition: Lemma ex_RInt_eval : forall prec prog bounds vars, contains_all bounds vars -> no_floor_prog prog = true -> forall a b xi, (forall x, Rmin a b <= x <= Rmax a b -> contains (I.convert xi) (Xreal x)) -> forall m, I.convert (nth m (eval prec prog (xi :: bounds)) I.nai) <> Inan -> ex_RInt (fun x => nth m (eval_real prog (x :: vars)) R0) a b.
proof: Proof. intros prec prog bounds vars H Hf a b xi Hx m HnotInan. apply: ex_RInt_continuous. intros z Hz. apply: continuous_eval HnotInan => //. exact: 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