proposition: Lemma TM_var_correct (x0 : R) (X0 X : I.type) : subset' (I.convert X0) (I.convert X) -> contains (I.convert X0) (Xreal x0) -> i_validTM x0 (I.convert X) (TM_var X X0) Xreal.
proof: Proof. move=> Hsubs Hx0. split=>//. apply I.mask_propagate_r. apply I.mask_correct', J.zero_correct. exact: Hsubs. exists (PolR.set_nth PolR.polyX 0 x0). apply: Pol.set_nth_correct =>//. exact: Pol.polyX_correct. move=> x Hx /=. replace (x - _)%R with 0%R by ring. apply I.mask_correct', J.zero_correct. 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