fact: Definition div_mixed_r prec xi y := match xi with | Ibnd xl xu => if F.real y then match F.cmp y F.zero with | Xlt => Ibnd (F.div_DN prec xu y) (F.div_UP prec xl y) | Xgt => Ibnd (F.div_DN prec xl y) (F.div_UP prec xu y) | _ => Inan end else Inan | Inan => Inan end.
imports: Coq(Bool Reals Psatz) Flocq(Raux) Stdlib Xreal Basic Sig Interval