fact: Definition f0eps_int (alpha : Z) (beta : nat) := let yi := f_int_fast (I.inv prec Epsilon) (- 2 - alpha) beta in if Nat.even beta then yi else I.neg yi.
imports: Coq(Reals ZArith Psatz Fourier_util) Flocq(Raux) Coquelicot(Coquelicot AutoDerive) mathcomp.ssreflect(ssreflect ssrfun ssrbool ssrnat bigop) Stdlib Coquelicot Xreal Interval