fact: Definition pi4_gen prec := I.sub prec (I.mul2 prec (I.mul2 prec (atan_fast0 prec (I.inv prec i5)))) (atan_fast0 prec (I.inv prec i239)).
imports: Coq(Reals Psatz) Flocq(Zaux Raux Digits) Stdlib Xreal Basic Sig Interval Float