fact: Definition wider prec xi yi := match yi, xi with | Inan, _ => false | Ibnd yl yu, Inan => true | Ibnd yl yu, Ibnd xl xu => let yw := F.sub_UP prec yu yl in if F.real yw then match F'.cmp (F.sub_UP prec xu xl) yw with | Xlt | Xeq => false | _ => true end else false end.
imports: Coq(Bool Reals Psatz) Flocq(Raux) Stdlib Xreal Basic Sig Interval