proposition: Theorem TM_var_correct_strong (x0 : R) (X0 X : I.type) (f : R -> ExtendedR) : subset' (I.convert X0) (I.convert X) -> contains (I.convert X0) (Xreal x0) -> (forall x : R, contains (I.convert X) (Xreal x) -> f x = Xreal x) -> i_validTM x0 (I.convert X) (TM_var X X0) f.
proof: Proof. move=> Hsubset Hx0 Hid. apply: TM_fun_eq; last apply: TM_var_correct Hsubset Hx0. by move=> *; rewrite Hid. 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