proposition: Lemma opp_slow_correct u (Y : I.type) tf f : approximates Y tf f -> approximates Y (opp_slow u Y tf) (fun x => Xneg (f x)).
proof: Proof. intros Hf Hne. now apply TM_opp_correct ; apply get_tm_correct. 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