proposition: Lemma TM_fun_eq f g (x0 : R) (X : interval) TMf : (forall x, contains X (Xreal x) -> f x = g x) -> i_validTM x0 X TMf f -> i_validTM x0 X TMf g.
proof: Proof. move=> Hfg [Hdom Hnai H0 Hsubs Hmain]. split=>//. move=> x Hx Dx. apply: (Hdom x) =>//. by rewrite Hfg. have [Q HQ Hf] := Hmain. exists Q =>//. move=> x Hx. rewrite -Hfg //. exact: Hf. Qed.
imports: Coq(ZArith Psatz Reals) Flocq(Raux) Coquelicot(Coquelicot) mathcomp.ssreflect(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype bigop) Stdlib MathComp Coquelicot Xreal Interval Basic Xreal_derive Interval_compl Datatypes Taylor_poly Basic_rec Bound