fact: Fixpoint expn_fast0_aux prec thre powi xi facti divi (nb : nat) { struct nb } := let npwi := I.mul prec powi xi in let vali := I.div prec npwi divi in match F'.cmp (I.upper vali) thre, nb with | Xlt, _ | _, O => I.bnd F.zero (I.upper vali) | _, S n => let nfacti := I.add prec facti i1 in let ndivi := I.mul prec divi facti in I.sub prec vali (expn_fast0_aux prec thre npwi xi nfacti ndivi n) end.
imports: Coq(Reals Psatz) Flocq(Zaux Raux Digits) Stdlib Xreal Basic Sig Interval Float