proposition: Lemma f_int_fast_f_int alpha beta : f_int_fast alpha beta = f_int alpha beta.
proof: Proof. elim: beta => [| beta Hbeta] //= . rewrite /f_int_fast //= . by rewrite -!Hbeta. Qed.
imports: Coq(Reals ZArith Psatz Fourier_util) Flocq(Raux) Coquelicot(Coquelicot AutoDerive) mathcomp.ssreflect(ssreflect ssrfun ssrbool ssrnat bigop) Stdlib Coquelicot Xreal Interval