proposition: Lemma TMset0_correct (x0 : R) (X : I.type) Mf f : let: A0 := Pol.nth (approx Mf) 0 in forall a0 alpha0, a0 >: alpha0 -> i_validTM x0 (I.convert X) Mf f -> i_validTM x0 (I.convert X) (TMset0 Mf (I.sub prec A0 a0)) (fun x => f x - Xreal alpha0).
proof: Proof. move=> a0 alpha0 in_a0 Hf. rewrite /TMset0. have [Mfdef Mfnai Mfzero Mfsubs Mfmain] := Hf. split ; try easy. intros x Hx Hfx. apply (Mfdef x Hx). revert Hfx ; clear. by case f. destruct Mfmain as [Q H1 H2]. exists (PolR.set_nth Q 0 (PolR.nth Q 0 - alpha0)%R). intros k. specialize (H1 k). clear - H1 in_a0. rewrite Pol.nth_set_nth PolR.nth_set_nth. destruct k as [|k] ; simpl. by apply (I.sub_correct _ _ _ _ (Xreal _) H1). exact H1. intros x Hx. specialize (H2 x Hx). move: (Mfdef x Hx). clear -H2. case Df: (f x) => [|fx]. by move ->. intros _. rewrite /Xbind2 /proj_val. replace (PolR.set_nth Q 0 (PolR.nth Q 0 - alpha0)%R).[x - x0] with (Q.[x - x0] - alpha0)%R. replace (fx - alpha0 - (Q.[x - x0] - alpha0))%R with (fx - Q.[x - x0])%R by ring. by rewrite Df in H2. destruct Q as [|q0 Q]. by rewrite /= Rmult_0_l Rplus_0_l. by rewrite /= /Rminus Rplus_assoc. 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