fact: Definition unary_bnd prec (o : unary_op) : I.type -> I.type := match o with | Neg => I.neg | Abs => I.abs | Inv => I.inv prec | Sqr => I.sqr prec | Sqrt => I.sqrt prec | Cos => I.cos prec | Sin => I.sin prec | Tan => I.tan prec | Atan => I.atan prec | Exp => I.exp prec | Ln => I.ln prec | PowerInt n => fun x => I.power_int prec x n | Nearbyint m => I.nearbyint m | RoundFlt m emin p => J.round_flt prec m emin p | ErrorFlt m emin p => I.error_flt prec m emin p | RoundFix m emin => J.round_fix prec m emin | ErrorFix m emin => I.error_fix prec m emin end.
imports: Coq(Reals List) Xreal Basic Interval