fact: Definition abs (u : U) (X : I.type) (t : T) : T := let e := eval u t X X in match I.sign_large e with | Xeq | Xgt => t | Xlt => opp u X t | Xund => Tm (TM_any u.1 (I.abs e) X u.2) 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