proposition: Lemma TM_sub_correct (x0 : R) (X : interval) (TMf TMg : rpa) f g : i_validTM x0 X TMf f -> i_validTM x0 X TMg g -> i_validTM x0 X (TM_sub TMf TMg) (fun xr => Xsub (f xr) (g xr)).
proof: Proof. move=> [Fdef Fnai Fzero Hsubset /= Fmain] [Gdef Gnai Gzero _ /= Gmain]. have HL : forall x : R, contains X (Xreal x) -> Xsub (f x) (g x) = Xnan -> I.convert (I.sub prec (error TMf) (error TMg)) = IInan. move=> x Hx. case Ef: (f x) => [|fx]. rewrite I.sub_propagate_l //; exact: Fdef Ef. case Eg: (g x) => [|gx //]. rewrite I.sub_propagate_r //; exact: Gdef Eg. split=>//=. by move=> HX; rewrite I.sub_propagate_l // Fnai. suff->: Xreal 0 = (Xreal 0 - Xreal 0)%XR by apply: I.sub_correct. by rewrite /= Rminus_0_r. move: Fmain Gmain => [pf Hf1 Hf2] [pg Hg1 Hg2]. exists (PolR.sub tt pf pg); first exact: Pol.sub_correct. move=> x Hx /=. rewrite PolR.horner_sub. case E0: (I.convert (I.sub prec _ _)) {HL} (HL x Hx) => [|zl zu] //. set pfx := pf.[_]; set pgx := pg.[_]. case Ef: f => [|fx]. by move => ->. case Eg: g => [|gx]. by move => ->. intros _. rewrite /Xbind2 /proj_val -E0. replace (fx - gx - (pfx - pgx))%R with ((fx - pfx) - (gx - pgx))%R by ring. apply: J.sub_correct. move: (Hf2 x Hx). by rewrite Ef. move: (Hg2 x Hx). by rewrite Eg. 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