fact: Definition f0eps_lim (alpha : Z) (beta : nat) (epsilon : R) := (-1) ^ beta * f_lim (- 2 - alpha) beta (/ epsilon).
imports: Coq(Reals ZArith Psatz Fourier_util) Flocq(Raux) Coquelicot(Coquelicot AutoDerive) mathcomp.ssreflect(ssreflect ssrfun ssrbool ssrnat bigop) Stdlib Coquelicot Xreal Interval