fact: Definition abs xi := match xi with | Ibnd xl xu => match sign_large_ xl xu with | Xgt => xi | Xeq => Ibnd F.zero F.zero | Xlt => Ibnd (F.neg xu) (F.neg xl) | Xund => Ibnd F.zero (F.max (F.neg xl) xu) end | Inan => Inan end.
imports: Coq(Bool Reals Psatz) Flocq(Raux) Stdlib Xreal Basic Sig Interval