proposition: Theorem opp_correct u (Y : I.type) tf f : approximates Y tf f -> approximates Y (opp u Y tf) (fun x => Xneg (f x)).
proof: Proof. move: tf => [cf| |tf] Hmain; try exact: opp_slow_correct. move=> Hne. destruct (Hmain Hne) as [H|[y Hy1 Hy2]]. left. now apply J.neg_propagate. right. exists (Xneg y); first exact: I.neg_correct. by move=> x Hx; rewrite /= Hy2. 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