fact: Definition atan prec xi := match xi with | Ibnd xl xu => Ibnd (if F.real xl then lower (T.atan_fast prec xl) else F.neg (F.mul_UP prec (upper (T.pi4 prec)) c2)) (if F.real xu then upper (T.atan_fast prec xu) else F.mul_UP prec (upper (T.pi4 prec)) c2) | Inan => Inan end.
imports: Coq(Reals Psatz) Xreal Basic Sig Interval Float Transcend