proposition: Theorem sub_correct u (Y : I.type) tf tg f g : approximates Y tf f -> approximates Y tg g -> approximates Y (sub u Y tf tg) (fun x => Xsub (f x) (g x)).
proof: Proof. move: tf tg => [cf| |tf] [cg| |tg] Hf Hg; try exact: sub_slow_correct. move=> Hne. move: Hf => /(_ Hne) [Hf|[yf Hyf1 /= Hyf2]]. left. now apply I.sub_propagate_l. move: Hg => /(_ Hne) [Hg|[yg Hyg1 /= Hyg2]]. left. now apply I.sub_propagate_r. right. exists (Xsub yf yg); first exact: I.sub_correct. by move=> x Hx; rewrite /= Hyf2 // Hyg2. Qed.
imports: Coq(Reals ZArith Psatz) mathcomp.ssreflect(ssreflect ssrbool ssrfun eqtype ssrnat seq bigop) Interval Xreal Basic Interval_compl Datatypes Taylor_model_sharp Bound Bound_quad Univariate_sig