fact: Definition mul prec xi yi := match xi, yi with | Ibnd xl xu, Ibnd yl yu => match sign_large_ xl xu, sign_large_ yl yu with | Xeq, _ => Ibnd F.zero F.zero | _, Xeq => Ibnd F.zero F.zero | Xgt, Xgt => Ibnd (F.mul_DN prec xl yl) (F.mul_UP prec xu yu) | Xlt, Xlt => Ibnd (F.mul_DN prec xu yu) (F.mul_UP prec xl yl) | Xgt, Xlt => Ibnd (F.mul_DN prec xu yl) (F.mul_UP prec xl yu) | Xlt, Xgt => Ibnd (F.mul_DN prec xl yu) (F.mul_UP prec xu yl) | Xgt, Xund => Ibnd (F.mul_DN prec xu yl) (F.mul_UP prec xu yu) | Xlt, Xund => Ibnd (F.mul_DN prec xl yu) (F.mul_UP prec xl yl) | Xund, Xgt => Ibnd (F.mul_DN prec xl yu) (F.mul_UP prec xu yu) | Xund, Xlt => Ibnd (F.mul_DN prec xu yl) (F.mul_UP prec xl yl) | Xund, Xund => Ibnd (F.min (F.mul_DN prec xl yu) (F.mul_DN prec xu yl)) (F.max (F.mul_UP prec xl yl) (F.mul_UP prec xu yu)) end | _, _ => Inan end.
imports: Coq(Bool Reals Psatz) Flocq(Raux) Stdlib Xreal Basic Sig Interval