fact: Definition expn_reduce prec x := let th := c1_8 in match F'.le' x th with | true => expn_fast0 (F.incr_prec prec 1) x | false => let m := F.StoZ (F.mag x) in let prec := F.incr_prec prec (Z2P (9 + m)) in let fix reduce x (nb : nat) {struct nb} := match F'.le' x th, nb with | true, _ => expn_fast0 prec x | _, O => I.bnd F.zero c1 | _, S n => I.sqr prec (reduce (F.div2 x) n) end in reduce x (8 + Z2nat m) end.
imports: Coq(Reals Psatz) Flocq(Zaux Raux Digits) Stdlib Xreal Basic Sig Interval Float