proposition: Lemma TM_opp_correct (x0 : R) (X : interval) (TMf : rpa) f : i_validTM x0 X TMf f -> i_validTM x0 X (TM_opp TMf) (fun xr => Xneg (f xr)).
proof: Proof. move=> [Hdef Hnai Hzero Hsubset /= Hmain]. have HL : forall x : R, contains X (Xreal x) -> Xneg (f x) = Xnan -> I.convert (I.neg (error TMf)) = IInan. move=> x Hx Dx. apply J.neg_propagate, (Hdef x Hx). by case: (f x) Dx. split=>//. by move=> HX; rewrite J.neg_propagate // Hnai. rewrite -Ropp_0. exact: J.neg_correct. have [Q H1 H2] := Hmain. exists (PolR.opp Q); first exact: Pol.opp_correct. move=> x Hx. rewrite PolR.horner_opp. case Efx: (f x) (H2 x Hx) => [|fx] /=. rewrite /Rminus 2!Rplus_0_l. exact: J.neg_correct. replace (- fx - - Q.[x - x0])%R with (-(fx - Q.[x - x0]))%R by ring. exact: J.neg_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