proposition: Lemma f_int_correct alpha beta (H : 0 < a) (Halpha: alpha <> (-1)%Z) : contains (I.convert (f_int alpha beta)) (Xreal (f_lim alpha beta a)).
proof: Proof. have Salphaneq0 : IZR (alpha + 1) <> 0. apply: not_0_IZR. by rewrite Z.add_move_0_r. have an0 : not (is_zero a). by move: is_zero_spec; case => // ; lra. have Salphaneq01: not (is_zero (IZR (alpha + 1))). move: (is_zero_spec (IZR (alpha + 1))). case => // . elim: beta => [|m HIm]. - rewrite /= . apply: J.div_correct. apply: J.neg_correct. apply: J.power_int_correct => // ; apply: Hcontainsa. exact: I.fromZ_correct. - rewrite /f_int -/f_int /f_lim -/f_lim. apply: J.sub_correct. apply: J.div_correct. apply: J.neg_correct. apply: J.mul_correct. apply: J.power_int_correct; apply: Hcontainsa. rewrite pow_powerRZ. apply: J.power_int_correct. apply: J.ln_correct; apply: Hcontainsa. exact: I.fromZ_correct. apply: J.mul_correct => // . apply: J.div_correct. by rewrite INR_IZR_INZ; apply: I.fromZ_correct. exact: I.fromZ_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