fact: Definition binary_bnd prec (o : binary_op) : I.type -> I.type -> I.type := match o with | Add => I.add prec | Sub => I.sub prec | Mul => I.mul prec | Div => I.div prec end.
imports: Coq(Reals List) Xreal Basic Interval