proposition: Lemma f_neg_int_correct beta : contains (I.convert (f_neg_int beta)) (Xreal (- f_neg a beta)).
proof: Proof. rewrite /f_neg Ropp_involutive. apply: J.inv_correct. apply: J.mul_correct. rewrite INR_IZR_INZ. exact: I.fromZ_correct. rewrite pow_powerRZ. apply: J.power_int_correct. exact: J.ln_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