fact: Definition div prec xi yi := match xi, yi with | Ibnd xl xu, Ibnd yl yu => match sign_strict_ xl xu, sign_strict_ yl yu with | _, Xund => Inan | _, Xeq => Inan | Xeq, _ => Ibnd F.zero F.zero | Xgt, Xgt => Ibnd (Fdivz_DN prec xl yu) (F.div_UP prec xu yl) | Xlt, Xlt => Ibnd (Fdivz_DN prec xu yl) (F.div_UP prec xl yu) | Xgt, Xlt => Ibnd (F.div_DN prec xu yu) (Fdivz_UP prec xl yl) | Xlt, Xgt => Ibnd (F.div_DN prec xl yl) (Fdivz_UP prec xu yu) | Xund, Xgt => Ibnd (F.div_DN prec xl yl) (F.div_UP prec xu yl) | Xund, Xlt => Ibnd (F.div_DN prec xu yu) (F.div_UP prec xl yu) end | _, _ => Inan end.
imports: Coq(Bool Reals Psatz) Flocq(Raux) Stdlib Xreal Basic Sig Interval