fact: Definition inv prec xi := match xi with | Ibnd xl xu => match sign_strict_ xl xu with | Xund => Inan | Xeq => Inan | _ => Ibnd (Fdivz_DN prec c1 xu) (Fdivz_UP prec c1 xl) end | _ => Inan end.
imports: Coq(Bool Reals Psatz) Flocq(Raux) Stdlib Xreal Basic Sig Interval