fact: Fixpoint atan_fast0_aux prec thre powi sqri divi (nb : nat) { struct nb } := let npwi := I.mul prec powi sqri 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 => I.sub prec vali (atan_fast0_aux prec thre npwi sqri (I.add prec divi i2) n) end.
imports: Coq(Reals Psatz) Flocq(Zaux Raux Digits) Stdlib Xreal Basic Sig Interval Float