proposition: Lemma f_int_fast_correct alpha beta (H : 0 < a) (Halpha: alpha <> (-1)%Z) : contains (I.convert (f_int_fast alpha beta)) (Xreal (f_lim alpha beta a)).
proof: Proof. by rewrite f_int_fast_f_int; exact: f_int_correct. Qed.
imports: Coq(Reals ZArith Psatz Fourier_util) Flocq(Raux) Coquelicot(Coquelicot AutoDerive) mathcomp.ssreflect(ssreflect ssrfun ssrbool ssrnat bigop) Stdlib Coquelicot Xreal Interval