fact: Definition cancel_add prec xi yi := match xi, yi with | Ibnd xl xu, Ibnd yl yu => Ibnd (F.sub_DN prec xl yl) (F.sub_UP prec xu yu) | _, _ => Inan end.
imports: Coq(Bool Reals Psatz) Flocq(Raux) Stdlib Xreal Basic Sig Interval