fact: Definition exp prec xi := match xi with | Ibnd xl xu => Ibnd (if F.real xl then lower (T.exp_fast prec xl) else F.zero) (if F.real xu then upper (T.exp_fast prec xu) else F.nan) | Inan => Inan end.
imports: Coq(Reals Psatz) Xreal Basic Sig Interval Float Transcend