proposition: Lemma f0eps_correct_sing alpha beta epsilon sing (B : R) (Heps : 0 < / B <= epsilon) (HB : 0 < B) (Halpha : (-1 < alpha)%Z) : is_RInt_gen ((fun x => powerRZ (x - sing) alpha * (pow (ln (x - sing)) beta))) (at_point (sing + / B)) (at_point (sing + epsilon)) (f0eps alpha beta epsilon B).
proof: Proof. apply is_RInt_gen_at_point. apply: (is_RInt_translation_sub _ (fun x => powerRZ x alpha * ln x ^ beta)). apply is_RInt_gen_at_point. have H : forall x y, x + y - x = y by move => x y; ring. rewrite !H; apply f0eps_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