proposition: Lemma continuous_eval : forall prec prog bounds vars, contains_all bounds vars -> no_floor_prog prog = true -> forall xi x, contains (I.convert xi) (Xreal x) -> forall m, I.convert (nth m (eval prec prog (xi :: bounds)) I.nai) <> Inan -> continuous (fun x => nth m (eval_real prog (x :: vars)) 0%R) x.
proof: Proof. intros prec prog bounds vars H Hf xi x Hx m HnotInan. apply: continuous_eval_ext => //. generalize (eval_correct_ext prec prog bounds vars H m xi (Xreal x) Hx). revert HnotInan. case I.convert => //. by case: (nth _ _ _). 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