proposition: Lemma TM_add_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_add TMf TMg) (fun xr => Xadd (f xr) (g xr)).
proof: Proof. move=> [Fdef Fnai Fzero Fsubs Fmain] [Gdef Gnai Gzero Gsubs Gmain]. have HL : forall x : R, contains X (Xreal x) -> Xadd (f x) (g x) = Xnan -> I.convert (I.add prec (error TMf) (error TMg)) = IInan. move=> x Hx. case Ef: (f x) => [|fx]. rewrite I.add_propagate_l //; exact: Fdef Ef. case Eg: (g x) => [|gx //]. rewrite I.add_propagate_r //; exact: Gdef Eg. split=>//=. by move=> H; move/(_ H) in Fnai; rewrite I.add_propagate_l. rewrite -(Rplus_0_l 0). exact: J.add_correct. move: Fmain Gmain => [pf Hf1 Hf2] [pg Hg1 Hg2]. exists (PolR.add tt pf pg); first exact: Pol.add_correct. move=> x Hx /=. rewrite PolR.horner_add. case E0: (I.convert (I.add 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 /proj_val /Xbind2 -E0. replace (fx + gx - (pfx + pgx))%R with ((fx - pfx) + (gx - pgx))%R by ring. apply: J.add_correct. rewrite -[fx](f_equal proj_val Ef). exact: Hf2. rewrite -[gx](f_equal proj_val Eg). exact: Hg2. 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