fact: Definition opp (u : U) (X : I.type) (t : T) : T := match t with | Const c => Const (I.neg c) | _ => opp_slow u X t end.
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