proposition: Lemma f0eps_correct (alpha : Z) (beta : nat) (Halpha : (alpha <> -1)%Z) : contains (I.convert (f0eps_int alpha beta)) (Xreal (f0eps_lim alpha beta epsilon)).
proof: Proof. rewrite /f0eps_int /f0eps_lim. assert (H: contains (I.convert (f_int_fast (I.inv prec Epsilon) (-2 - alpha) beta)) (Xreal (f_lim (-2 - alpha) beta (/ epsilon)))). { rewrite f_int_fast_f_int. apply: f_int_correct. exact: J.inv_correct. exact: Rinv_0_lt_compat. by lia. } replace ((-1) ^ beta) with (if Nat.even beta then 1 else -1). { case Nat.even. now rewrite Rmult_1_l. replace (-1 * _) with (-f_lim (-2 - alpha) beta (/ epsilon)) by ring. exact: J.neg_correct. } clear ; induction beta. easy. rewrite Nat.even_succ -Nat.negb_even. rewrite /= -IHbeta. case Nat.even => /= ; ring. Qed.
imports: Coq(Reals ZArith Psatz Fourier_util) Flocq(Raux) Coquelicot(Coquelicot AutoDerive) mathcomp.ssreflect(ssreflect ssrfun ssrbool ssrnat bigop) Stdlib Coquelicot Xreal Interval