fact: Definition exp_fast prec x := match F'.cmp x F.zero with | Xeq => i1 | Xlt => expn_reduce prec (F.neg x) | Xgt => let prec := F.incr_prec prec 1 in match I.invnz prec (expn_reduce prec x) with | Ibnd _ _ as b => b | Inai => I.bnd c1 F.nan end | Xund => I.nai end.
imports: Coq(Reals Psatz) Flocq(Zaux Raux Digits) Stdlib Xreal Basic Sig Interval Float