proposition: Lemma mul_slow_correct u (Y : I.type) tf tg f g : approximates Y tf f -> approximates Y tg g -> approximates Y (mul_slow u Y tf tg) (fun x => Xmul (f x) (g x)).
proof: Proof. intros Hf Hg Hne. apply TM_mul_correct ; try apply get_tm_correct ; try easy. exact: J.contains_midpoint. 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