fact: Definition ln_fast prec x := match F.cmp x F.zero with | Xgt => let xi := I.bnd x x in match F.cmp x c1 with | Xeq => I.zero | Xlt => let m := Z.opp (F.StoZ (F.mag (F.sub_UP prec c1 x))) in let prec := F.incr_prec prec (Z2P m) in I.neg (ln_fast1P prec (I.inv prec xi)) | Xgt => if F.real x then ln_fast1P prec xi else I.nai | Xund => I.nai end | _ => I.nai end.
imports: Coq(Reals Psatz) Flocq(Zaux Raux Digits) Stdlib Xreal Basic Sig Interval Float