fact: Definition unary_real (o : unary_op) : R -> R := match o with | Neg => Ropp | Abs => Rabs | Inv => Rinv | Sqr => Rsqr | Sqrt => sqrt | Cos => cos | Sin => sin | Tan => tan | Atan => atan | Exp => exp | Ln => ln | PowerInt n => fun x => powerRZ x n | Nearbyint m => Rnearbyint m | RoundFlt m emin prec => round_flt m emin prec | ErrorFlt m emin prec => fun x => Rminus (round_flt m emin prec x) x | RoundFix m emin => round_fix m emin | ErrorFix m emin => fun x => Rminus (round_fix m emin x) x end.
imports: Coq(Reals List) Xreal Basic Interval