fact: Definition ln_fast1P prec xi := let th := c1_p_c1_8 in match F'.le' (I.upper xi) th with | true => ln1p_fast0 prec (I.sub prec xi i1) | false => let m := Digits.Zdigits2 (F.StoZ (F.mag (I.upper xi))) in let prec := F.incr_prec prec 10 in let fix reduce xi (nb : nat) {struct nb} := match F'.le' (I.upper xi) th, nb with | true, _ => ln1p_fast0 prec (I.sub prec xi i1) | _, O => I.bnd F.zero F.nan | _, S n => I.mul2 prec (reduce (I.sqrt prec xi) n) end in reduce xi (8 + Z2nat m) end.
imports: Coq(Reals Psatz) Flocq(Zaux Raux Digits) Stdlib Xreal Basic Sig Interval Float